19/11/21 14:05:02 W0+ORYap.net
Feit-Thompson定理（英語版）は、Coqで2012年9月に証明が完了したという
同じことを、いま人手でやっても、いまや評価されないってことよ（単なる証明屋さん）
Coqよりも、人間に近い証明とか
人間に分かり易く、「Coqのやった証明が説明できる」とか
そういう人が、
評価されるようになるだろうね
URLﾘﾝｸ(ja.wikipedia.org)
Coq
(抜粋)
Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。
Coqには証明の自動化機能が増えている。中にはomegaタクティクというものがあり、プレスバーガー算術の大部分を決定できる。
Coqの最大の達成の中には、
・四色定理: Georges GonthierとBenjamin Wernerによって、完全に機械化された証明が2004年に完了した。[2]
・CompCert: C言語のコンパイラで、Coqによって開発され証明がつき、2006年にリリースされた。[3]
・Feit-Thompson定理（英語版）: Georges Gonthierと彼のグループによって、2012年9月に証明が完了した。[4]
がある。
CoqはGNU LGPLライセンスで配布されているフリーソフトウェアである。