[過去ﾛｸﾞ]
Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
Inter-universal geometry と ABC予想 49 http://rio2016.5ch.net/test/read.cgi/math/1586650355/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
978: １３２人目の素数さん [sage] 2020/04/15(水) 11:19:36.47 ID:r8DbtXP/ >>824 ＤＨＡを豊富に含んだ食品摂取で頭が良くなるって本当なんでしょうか? 最近話題になってたヨーロッパの天才児の食生活についても 「お魚を良く食べます」 ってお母様が仰ってました http://rio2016.5ch.net/test/read.cgi/math/1586650355/978
979: １３２人目の素数さん [sage] 2020/04/15(水) 12:15:15.85 ID:upGWUHod ブンゲン 「（数学的に正しいとは）水も漏らさぬ証明があること」「いかなる細部にも飛躍があってはならない」 よくぞ言った。 ブンゲン含め望月応援団は3.12→3.13の論証が、いかなる細部にも飛躍がない、 水も漏らさぬ証明であることを天下に示すべきである。 そのためには機械による検証が必要である。 それがないかぎりは、望月の証明は「数学的に正しい」とみとめられない。 http://rio2016.5ch.net/test/read.cgi/math/1586650355/979
980: １３２人目の素数さん [sage] 2020/04/15(水) 12:15:47.31 ID:upGWUHod ごめん、3.11→3.12 http://rio2016.5ch.net/test/read.cgi/math/1586650355/980
981: １３２人目の素数さん [] 2020/04/15(水) 12:57:01.17 ID:QCk3Iyvt Woitのブログ上で建設的な議論が進んでいるように見える 内容はわからないけど、とにかくややこしい問題だということだけはわかる http://rio2016.5ch.net/test/read.cgi/math/1586650355/981
982: １３２人目の素数さん [sage] 2020/04/15(水) 12:59:04.23 ID:1rZ9apod もう理解度と読み込みではIUTはショルツのもの。 http://rio2016.5ch.net/test/read.cgi/math/1586650355/982
983: １３２人目の素数さん [sage] 2020/04/15(水) 12:59:36.46 ID:LTi2Xsr9 >>979-980 １．有限単純群の分類で、2012年 証明支援言語Coqを用いたファイト・トンプソンの定理(1963)の機械的チェックの成功をアナウンスした しかし、その他の大部分は 機械的チェックなしなのです ２．1983 ゴーレンシュタインが、分類の証明が完了したとアナウンスした後、実は大穴が明いていることが判明(下記) ３．2004 アシュバッハーとスミス（ドイツ語版）が準薄群（すなわち偶数標数の体上の多くともランク2のリー型の群）について彼らの仕事を出版し、この時点で知られている分類の最後のギャップが埋められた ４．2008 原田とソロモンがマシュー群 M22（英語版） をカバーする、標準成分をもつ群についての分類の小さなギャップを埋めた。まあ、小さなピンホールがあったんだねｗ ５．証明支援言語Coqを用いた 機械的チェックは、後追いでしかない １）機械にインプットするデータに誤りがあれば、アウトプットは正しくない ２）証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？ ６．ゆえに、証明支援言語Coqを用いた 機械的チェックは、人間の証明の裏付けにすぎない。現状ではね。まずは、人間の証明が先です！ (参考) https://ja.wikipedia.org/wiki/%E6%9C%89%E9%99%90%E5%8D%98%E7%B4%94%E7%BE%A4%E3%81%AE%E5%88%86%E9%A1%9E 有限単純群の分類 (抜粋) 証明の歴史 1963 ファイトとトンプソンがファイト・トンプソンの定理（奇数位数定理）（英語版）を証明した。 1983 ゴーレンシュタインが、分類の証明が完了したとアナウンスした。しかし準薄（英語版）ケースの証明が不完全であったため、これは尚早であった 2004 アシュバッハーとスミス（ドイツ語版）が準薄群（すなわち偶数標数の体上の多くともランク2のリー型の群）について彼らの仕事を出版し、この時点で知られている分類の最後のギャップが埋められた 2008 原田とソロモンがマシュー群 M22（英語版） をカバーする、標準成分をもつ群についての分類の小さなギャップを埋めた。これは M22 のシューア乗数（英語版）についての計算において、誤って証明に欠落が生じていたためである 2012 ジョルジュ・ゴンティエ（英語版）とその共同研究者達が、証明支援言語Coqを用いたファイト・トンプソンの定理の機械的チェックの成功をアナウンスした http://rio2016.5ch.net/test/read.cgi/math/1586650355/983
984: １３２人目の素数さん [] 2020/04/15(水) 13:06:47.91 ID:/g+JzMtk >>983 ＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？ Coqの正当性をCoqで検証すればいいんじゃね？ http://rio2016.5ch.net/test/read.cgi/math/1586650355/984
985: １３２人目の素数さん [] 2020/04/15(水) 13:10:33.74 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/985
986: １３２人目の素数さん [] 2020/04/15(水) 13:13:18.65 ID:QCk3Iyvt >>985 そのプログラムの正当性はどうやって検証するの？ http://rio2016.5ch.net/test/read.cgi/math/1586650355/986
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
0.016s