[過去ﾛｸﾞ]
Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
Inter-universal geometry と ABC予想 49 http://rio2016.5ch.net/test/read.cgi/math/1586650355/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
987: １３２人目の素数さん [] 2020/04/15(水) 13:13:33.97 ID:/g+JzMtk >>984 具体的に説明するか Coq証明系の存在証明をCoqで書いて プログラムとして抽出すればいいってこと カリー＝ハワード同型対応 https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C http://rio2016.5ch.net/test/read.cgi/math/1586650355/987
988: １３２人目の素数さん [] 2020/04/15(水) 13:15:03.88 ID:/g+JzMtk >>986 抽出されたプログラムにもう一度証明を食わせて 同じプログラムが抽出されればOK http://rio2016.5ch.net/test/read.cgi/math/1586650355/988
989: １３２人目の素数さん [sage] 2020/04/15(水) 13:16:45.50 ID:LTi2Xsr9 >>988 インプットデータの正当性は？ http://rio2016.5ch.net/test/read.cgi/math/1586650355/989
990: １３２人目の素数さん [sage] 2020/04/15(水) 13:22:26.67 ID:LTi2Xsr9 >>987 カリー＝ハワード同型対応 は正しいが Coqにそれが正しく実装されている保証がない ゆえに、ふつうは二つの異なる証明系に食わせて、結果の一致までを見ることで精度上げることはよくやられる １．もし、人間の証明と機械の証明結果が一致すれば、人の証明が正しい裏付けになる ２．もし、人間の証明と機械の証明結果が一致しない場合、人の証明が間違っている可能性が高いが、機械への入力ミスなどの可能捨てきれない よって、人間の証明を、人が 再チェックして、確認することになるだろう http://rio2016.5ch.net/test/read.cgi/math/1586650355/990
991: １３２人目の素数さん [] 2020/04/15(水) 13:22:59.13 ID:QCk3Iyvt よくわかんないけどそのやり方で検証と言えるのかな なんか正しいから正しいと言っているように見えるんだけど http://rio2016.5ch.net/test/read.cgi/math/1586650355/991
992: １３２人目の素数さん [] 2020/04/15(水) 13:25:21.63 ID:/g+JzMtk >>989 漫然とインプットデータといわれても困る 公理や定理の式が正しいとして、証明が間違っていたら？ということはない 公理や定理の式が間違っていたら？ それは検証系で検査できることではない プログラム検証のV&Vで、 後のV(verification 検証)は機械的にできるが 前のV(varidation 妥当性確認）は機械で実施するものではない https://www.ipa.go.jp/files/000036457.pdf http://rio2016.5ch.net/test/read.cgi/math/1586650355/992
993: １３２人目の素数さん [sage] 2020/04/15(水) 13:26:31.69 ID:LTi2Xsr9 >>990 > よって、人間の証明を、人が >再チェックして、確認することになるだろう だったら、状況はいまとあまり変わらないんじゃない？ Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど http://rio2016.5ch.net/test/read.cgi/math/1586650355/993
994: １３２人目の素数さん [] 2020/04/15(水) 13:27:59.69 ID:/g+JzMtk >>992 誤 varidation 正 validation http://rio2016.5ch.net/test/read.cgi/math/1586650355/994
995: １３２人目の素数さん [sage] 2020/04/15(水) 13:29:04.99 ID:LTi2Xsr9 >>993 ＞Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど たとえば、IUTの原稿ファイル貰って、それをCoqが機械読みしてくれなら簡単だが もし、人が読んで、Coq入力を作るなら、それはすぐにはできないよね http://rio2016.5ch.net/test/read.cgi/math/1586650355/995
996: １３２人目の素数さん [] 2020/04/15(水) 13:30:09.19 ID:/g+JzMtk >>993 そもそも、理論として出来上がっているかどうかが疑問視されているなら Coqへの実装は無意味ではないだろう http://rio2016.5ch.net/test/read.cgi/math/1586650355/996
997: １３２人目の素数さん [] 2020/04/15(水) 13:31:03.89 ID:/g+JzMtk >>995 もちろん、すぐにはできないが、やらない言い訳はないな http://rio2016.5ch.net/test/read.cgi/math/1586650355/997
998: １３２人目の素数さん [] 2020/04/15(水) 13:39:57.69 ID:/g+JzMtk >>990 Coqによる検証でも、人間によるテストを全部無くすことはできないが 「人間の証明を、人が再チェックして、確認する」 とかいう機械排除の口実は全く存在しない http://rio2016.5ch.net/test/read.cgi/math/1586650355/998
999: １３２人目の素数さん [sage] 2020/04/15(水) 14:26:02.19 ID:upGWUHod >>983->>998 のやり取りみるだけで、擁護派は数学的真理などどうでもよく、 機械検証をいわれたら逃げ回り、 ひたすら「望月がABC予想を証明した功績を認めろ」と強弁しているだけであることがわかる。 http://rio2016.5ch.net/test/read.cgi/math/1586650355/999
1000: １３２人目の素数さん [] 2020/04/15(水) 14:27:54.76 ID:upGWUHod それが結論 http://rio2016.5ch.net/test/read.cgi/math/1586650355/1000
1001: 1001 [] ID:Thread このスレッドは１０００を超えました。 新しいスレッドを立ててください。 life time: 3日 5時間 15分 19秒 http://rio2016.5ch.net/test/read.cgi/math/1586650355/1001
1002: 1002 [] ID:Thread 5ちゃんねるの運営はプレミアム会員の皆さまに支えられています。 運営にご協力お願いいたします。 ─────────────────── 《プレミアム会員の主な特典》 ★ 5ちゃんねる専用ブラウザからの広告除去 ★ 5ちゃんねるの過去ログを取得 ★ 書き込み規制の緩和 ─────────────────── 会員登録には個人情報は一切必要ありません。 月300円から匿名でご購入いただけます。 ▼ プレミアム会員登録はこちら ▼ https://premium.5ch.net/ ▼ 浪人ログインはこちら ▼ https://login.5ch.net/login.php http://rio2016.5ch.net/test/read.cgi/math/1586650355/1002
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
1.738s*