[過去ﾛｸﾞ]
現代数学の系譜 工学物理雑談 古典ガロア理論も読む79 (1002ﾚｽ)
現代数学の系譜 工学物理雑談 古典ガロア理論も読む79 http://rio2016.5ch.net/test/read.cgi/math/1573769803/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制
です｡10分ほどで解除するので､
他のﾌﾞﾗｳｻﾞ
へ避難してください｡
72: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [] 2019/11/21(木) 14:05:02.28 ID:W0+ORYap Feit-Thompson定理（英語版）は、Coqで2012年9月に証明が完了したという 同じことを、いま人手でやっても、いまや評価されないってことよ（単なる証明屋さん） Coqよりも、人間に近い証明とか 人間に分かり易く、「Coqのやった証明が説明できる」とか そういう人が、 評価されるようになるだろうね https://ja.wikipedia.org/wiki/Coq 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ライセンスで配布されているフリーソフトウェアである。 http://rio2016.5ch.net/test/read.cgi/math/1573769803/72
73: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [] 2019/11/21(木) 14:09:43.87 ID:W0+ORYap >>72 ＞Feit-Thompson定理（英語版）は、Coqで2012年9月に証明が完了したという ＞同じことを、いま人手でやっても、いまや評価されないってことよ（単なる証明屋さん） いや、もちろん、Coqに掛からない証明も沢山あるし 最初からは、Coqには掛からないのかも知れない そういう場合に、 手作業での場合分け証明は、世界初としては評価されるよ あるいは、Coqに掛けられるように腑分けして その後、Coqに掛けて証明を終えるとか そういうことのできる人は、 評価されるだろうね http://rio2016.5ch.net/test/read.cgi/math/1573769803/73
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.053s