[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
987(1): 2020/04/15(水)13:13 ID:/g+JzMtk(3/9) AAS
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org
988(1): 2020/04/15(水)13:15 ID:/g+JzMtk(4/9) AAS
>>986
抽出されたプログラムにもう一度証明を食わせて
同じプログラムが抽出されればOK
989(1): 2020/04/15(水)13:16 ID:LTi2Xsr9(2/5) AAS
>>988
インプットデータの正当性は？
990(2): 2020/04/15(水)13:22 ID:LTi2Xsr9(3/5) AAS
>>987
カリー＝ハワード同型対応
は正しいが
Coqにそれが正しく実装されている保証がない
ゆえに、ふつうは二つの異なる証明系に食わせて、結果の一致までを見ることで精度上げることはよくやられる
１．もし、人間の証明と機械の証明結果が一致すれば、人の証明が正しい裏付けになる
２．もし、人間の証明と機械の証明結果が一致しない場合、人の証明が間違っている可能性が高いが、機械への入力ミスなどの可能捨てきれない
省2
991: 2020/04/15(水)13:22 ID:QCk3Iyvt(3/3) AAS
よくわかんないけどそのやり方で検証と言えるのかな
なんか正しいから正しいと言っているように見えるんだけど
992(1): 2020/04/15(水)13:25 ID:/g+JzMtk(5/9) AAS
>>989
漫然とインプットデータといわれても困る
公理や定理の式が正しいとして、証明が間違っていたら？ということはない
公理や定理の式が間違っていたら？ それは検証系で検査できることではない
プログラム検証のV&Vで、
後のV(verification 検証)は機械的にできるが
前のV(varidation 妥当性確認）は機械で実施するものではない
省1
993(2): 2020/04/15(水)13:26 ID:LTi2Xsr9(4/5) AAS
>>990
> よって、人間の証明を、人が
>再チェックして、確認することになるだろう
だったら、状況はいまとあまり変わらないんじゃない？
Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
994(1): 2020/04/15(水)13:27 ID:/g+JzMtk(6/9) AAS
>>992
誤 varidation
正 validation
995(1): 2020/04/15(水)13:29 ID:LTi2Xsr9(5/5) AAS
>>993
＞Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
たとえば、IUTの原稿ファイル貰って、それをCoqが機械読みしてくれなら簡単だが
もし、人が読んで、Coq入力を作るなら、それはすぐにはできないよね
996: 2020/04/15(水)13:30 ID:/g+JzMtk(7/9) AAS
>>993
そもそも、理論として出来上がっているかどうかが疑問視されているなら
Coqへの実装は無意味ではないだろう
997: 2020/04/15(水)13:31 ID:/g+JzMtk(8/9) AAS
>>995
もちろん、すぐにはできないが、やらない言い訳はないな
998(1): 2020/04/15(水)13:39 ID:/g+JzMtk(9/9) AAS
>>990
Coqによる検証でも、人間によるテストを全部無くすことはできないが
「人間の証明を、人が再チェックして、確認する」
とかいう機械排除の口実は全く存在しない
999: 2020/04/15(水)14:26 ID:upGWUHod(3/4) AAS
>>983->>998
のやり取りみるだけで、擁護派は数学的真理などどうでもよく、
機械検証をいわれたら逃げ回り、
ひたすら「望月がABC予想を証明した功績を認めろ」と強弁しているだけであることがわかる。
1000: 2020/04/15(水)14:27 ID:upGWUHod(4/4) AAS
それが結論
1001(1): 1001 ID:Thread(1/2) AAS
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 3日 5時間 15分 19秒
1002(1): 1002 ID:Thread(2/2) AAS
5ちゃんねるの運営はプレミアム会員の皆さまに支えられています。
運営にご協力お願いいたします。
───────────────────
《プレミアム会員の主な特典》
★ 5ちゃんねる専用ブラウザからの広告除去
★ 5ちゃんねるの過去ログを取得
★ 書き込み規制の緩和
省7
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 1.791s*