[過去ﾛｸﾞ] 現代数学の系譜 工学物理雑談 古典ガロア理論も読む79 (1002ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
72(1): 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE 2019/11/21(木)14:05 ID:W0+ORYap(6/7) AAS
Feit-Thompson定理（英語版）は、Coqで2012年9月に証明が完了したという
同じことを、いま人手でやっても、いまや評価されないってことよ（単なる証明屋さん）
Coqよりも、人間に近い証明とか
人間に分かり易く、「Coqのやった証明が説明できる」とか
そういう人が、
評価されるようになるだろうね
外部ﾘﾝｸ:ja.wikipedia.org
Coq
(抜粋)
Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。
省7
73: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE 2019/11/21(木)14:09 ID:W0+ORYap(7/7) AAS
>>72
＞Feit-Thompson定理（英語版）は、Coqで2012年9月に証明が完了したという
＞同じことを、いま人手でやっても、いまや評価されないってことよ（単なる証明屋さん）
いや、もちろん、Coqに掛からない証明も沢山あるし
最初からは、Coqには掛からないのかも知れない
そういう場合に、
手作業での場合分け証明は、世界初としては評価されるよ
あるいは、Coqに掛けられるように腑分けして
その後、Coqに掛けて証明を終えるとか
そういうことのできる人は、
省1
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.187s*