20/04/15 12:59:04.23 1rZ9apod.net
もう理解度と読み込みではIUTはショルツのもの。
1026:１３２人目の素数さん
20/04/15 12:59:36.46 LTi2Xsr9.net
>>979-980
１．有限単純群の分類で、2012年 証明支援言語Coqを用いたファイト・トンプソンの定理(1963)の機械的チェックの成功をアナウンスした
しかし、その他の大部分は 機械的チェックなしなのです
２．1983 ゴーレンシュタインが、分類の証明が完了したとアナウンスした後、実は大穴が明いていることが判明(下記)
３．2004 アシュバッハーとスミス（ドイツ語版）が準薄群（すなわち偶数標数の体上の多くともランク2のリー型の群）について彼らの仕事を出版し、この時点で知られている分類の最後のギャップが埋められた
４．2008 原田とソロモンがマシュー群 M22（英語版） をカバーする、標準成分をもつ群についての分類の小さなギャップを埋めた。まあ、小さなピンホールがあったんだねｗ
５．証明支援言語Coqを用いた 機械的チェックは、後追いでしかない
１）機械にインプットするデータに誤りがあれば、アウトプットは正しくない
２）証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？
６．ゆえに、証明支援言語Coqを用いた 機械的チェックは、人間の証明の裏付けにすぎない。現状ではね。まずは、人間の証明が先です！
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
有限単純群の分類
(抜粋)
証明の歴史
1963 ファイトとトンプソンがファイト・トンプソンの定理（奇数位数定理）（英語版）を証明した。
1983 ゴーレンシュタインが、分類の証明が完了したとアナウンスした。しかし準薄（英語版）ケースの証明が不完全であったため、これは尚早であった
2004 アシュバッハーとスミス（ドイツ語版）が準薄群（すなわち偶数標数の体上の多くともランク2のリー型の群）について彼らの仕事を出版し、この時点で知られている分類の最後のギャップが埋められた
2008 原田とソロモンがマシュー群 M22（英語版） をカバーする、標準成分をもつ群についての分類の小さなギャップを埋めた。これは M22 のシューア乗数（英語版）についての計算において、誤って証明に欠落が生じていたためである
2012 ジョルジュ・ゴンティエ（英語版）とその共同研究者達が、証明支援言語Coqを用いたファイト・トンプソンの定理の機械的チェックの成功をアナウンスした
1027:１３２人目の素数さん
20/04/15 13:06:47 /g+JzMtk.net
>>983
＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？
Coqの正当性をCoqで検証すればいいんじゃね？
1028:１３２人目の素数さん
20/04/15 13:10:33 /g+JzMtk.net
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
URLﾘﾝｸ(ja.wikipedia.org)
1029:１３２人目の素数さん
20/04/15 13:13:18 QCk3Iyvt.net
>>985
そのプログラムの正当性はどうやって検証するの？
1030:１３２人目の素数さん
20/04/15 13:13:33 /g+JzMtk.net
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
URLﾘﾝｸ(ja.wikipedia.org)
1031:１３２人目の素数さん
20/04/15 13:15:03 /g+JzMtk.net
>>986
抽出されたプログラムにもう一度証明を食わせて
同じプログラムが抽出されればOK
1032:１３２人目の素数さん
20/04/15 13:16:45 LTi2Xsr9.net
>>988
インプットデータの正当性は？
1033:１３２人目の素数さん
20/04/15 13:22:26.67 LTi2Xsr9.net
>>987
カリー＝ハワード同型対応
は正しいが
Coqにそれが正しく実装されている保証がない
ゆえに、ふつうは二つの異なる証明系に食わせて、結果の一致までを見ることで精度上げることはよくやられる
１．もし、人間の証明と機械の証明結果が一致すれば、人の証明が正しい裏付けになる
２．もし、人間の証明と機械の証明結果が一致しない場合、人の証明が間違っている可能性が高いが、機械への入力ミスなどの可能捨てきれない
よって、人間の証明を、人が
再チェックして、確認することになるだろう
1034:１３２人目の素数さん
20/04/15 13:22:59.13 QCk3Iyvt.net
よくわかんないけどそのやり方で検証と言えるのかな
なんか正しいから正しいと言っているように見えるんだけど
1035:１３２人目の素数さん
20/04/15 13:25:21.63 /g+JzMtk.net
>>989
漫然とインプットデータといわれても困る
公理や定理の式が正しいとして、証明が間違っていたら？ということはない
公理や定理の式が間違っていたら？ それは検証系で検査できることではない
プログラム検証のV&Vで、
後のV(verification 検証)は機械的にできるが
前のV(varidation 妥当性確認）は機械で実施するものではない
URLﾘﾝｸ(www.ipa.go.jp)
1036:１３２人目の素数さん
20/04/15 13:26:31.69 LTi2Xsr9.net
>>990
> よって、人間の証明を、人が
>再チェックして、確認することになるだろう
だったら、状況はいまとあまり変わらないんじゃない？
Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
1037:１３２人目の素数さん
20/04/15 13:27:59.69 /g+JzMtk.net
>>992
誤 varidation
正 validation
1038:１３２人目の素数さん
20/04/15 13:29:04.99 LTi2Xsr9.net
>>993
＞Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
たとえば、IUTの原稿ファイル貰って、それをCoqが機械読みしてくれなら簡単だが
もし、人が読んで、Coq入力を作るなら、それはすぐにはできないよね
1039:１３２人目の素数さん
20/04/15 13:30:09.19 /g+JzMtk.net
>>993
そもそも、理論として出来上がっているかどうかが疑問視されているなら
Coqへの実装は無意味ではないだろう
1040:１３２人目の素数さん
20/04/15 13:31:03.89 /g+JzMtk.net
>>995
もちろん、すぐにはできないが、やらない言い訳はないな
1041:１３２人目の素数さん
20/04/15 13:39:57 /g+JzMtk.net
>>990
Coqによる検証でも、人間によるテストを全部無くすことはできないが
「人間の証明を、人が再チェックして、確認する」
とかいう機械排除の口実は全く存在しない
1042:１３２人目の素数さん
20/04/15 14:26:02.19 upGWUHod.net
>>983->>998
のやり取りみるだけで、擁護派は数学的真理などどうでもよく、
機械検証をいわれたら逃げ回り、
ひたすら「望月がABC予想を証明した功績を認めろ」と強弁しているだけであることがわかる。
1043:１３２人目の素数さん
20/04/15 14:27:54.76 upGWUHod.net
それが結論
1044:1001
Over 1000 Thread.net
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 3日 5時間 15分 19秒
1045:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています