20/04/15 02:19:40 XXGhTXIb.net
擁護派が優勢になりつつあるのでは？
WはDavid Robertsの解説を読んで望月さんの視点に気が付いたようで、理解を示しつつありますね。
Dupuy,UF,Robertsの突っ込みに対しScholzeがまともに応える事ができるのか、それともお茶を濁して逃げるのかで、彼が数学者としての
誠実さを本当に持ち合わせているのかを見極められると思います。
1001:１３２人目の素数さん
20/04/15 02:36:21 sDPcsM6G.net
>>956
Wは、Dupuyにアドバイス（I’m just saying that you can reverse the argument to an extent. 私はあなたが議論をある程度逆転させることができると言っているだけです。）してましたね。
その後にDupuyが（Will（＝W)’s comment has insprired me to write a little bit more since he seems to be paying close attention (thank you Will)
と礼を述べてから、Scholzeの主張の1)、2)のおかしな点に突っ込みを入れたので、Wは最初から理解をしていたのだと思いますよ。
1002:１３２人目の素数さん
20/04/15 02:47:41 GMXF0IZY.net
一般的な用語を勝手に違う解釈で使ったのならばアンドとオアを間違えてる方はどっちなんですかね
1003:１３２人目の素数さん
20/04/15 04:22:36 PZKJ5Zxj.net
Wって誰？
1004:粋蕎
20/04/15 05:36:00.34 FI0JUvCQ.net
ヲイト氏の事とは違うん？
1005:１３２人目の素数さん
20/04/15 05:38:50 xeYb99iT.net
Williamです
1006:１３２人目の素数さん
20/04/15 05:54:49 38p90lrI.net
自分の考えを披露してショルツに考えてもらう感じだな
ショルツがそれなら可能性はあるかもしれないって言うか、全否定するか
ショルツにIUTを解いてもらう解決だな
1007:１３２人目の素数さん
20/04/15 06:05:03.41 gAHsVD46.net
それもうショルツの定理だろ
1008:１３２人目の素数さん
20/04/15 07:38:11 Rsdt7V/S.net
>>946
>S・Sはあっさり書いているが、当然望月氏も知っているはずだろうと思って書いていたはず。
>これは“Faltings’ theorem (Shafarevich conjecture) applied to the Weil restriction”した場合の話だよ。
>Finite Weil restriction of curves
レベルが高すぎて、すぐにはついていけないが
その話は、引用文献の下記のことかな？
URLﾘﾝｸ(link.springer.com)
Open Access
Published: 03 December 2014
Finite Weil restriction of curves
E. V. Flynn & D. Testa
Monatshefte fur Mathematik volume 176, pages197?218(2015)
(抜粋)
Cases where Faltings’ theorem does not apply
In this section we analyze the cases where the relative Weil restriction of a morphism of curves contains a component of geometric genus at most one.
In such cases, Faltings’ theorem cannot be applied to deduce the finiteness of rational points of the relative Weil restriction and we find explicit non-tautological examples in which these sets of rational points are infinite.
The following remark is an immediate consequence of Faltings’ theorem and guides the choice of cases we handle in this section.
1009:１３２人目の素数さん
20/04/15 08:11:24.56 XXGhTXIb.net
ショルツはAnabelian geometryの基本が全く理解できていないというDupuyのダメだしが炸裂しましたね。
>>957
>Wは最初から理解をしていたのだと思いますよ
なるほど、改めて読んでみたら流れを理解できました。
1010:１３２人目の素数さん
20/04/15 08:35:51 TgZzPWYt.net
今ショルツが再び読み直してる感じなのか どうなるのかな
1011:１３２人目の素数さん
20/04/15 08:47:30 ZCZL7ADF.net
次スレ
Inter-universal geometry と ABC予想 50
ｽﾚﾘﾝｸ(math板)
1012:１３２人目の素数さん
20/04/15 09:05:52.89 WpCBiVcM.net
擁護派のコメントは望月本人のものでなければ、迷惑でしかないレベル
1013:１３２人目の素数さん
20/04/15 09:17:22.17 Qr7I0O19.net
さいごはモッチーが勝ち、無冠の帝王になるにすーぱーもっちくん
1014:１３２人目の素数さん
20/04/15 09:31:58.92 TgZzPWYt.net
ショルツは読み直してるのではなく、すでに相当理解していて、
擁護派のDupy氏が逆にショルツに質問、ショルツが解説している
（否定的に）ショルツの考えが変わる感じではなさそう
1015:１３２人目の素数さん
20/04/15 10:33:58.74 +ag2Wthg.net
望月-ショルツの定理と呼ぶか
ショルツ-望月の定理と呼ぶかで100スレ消費
に10モッチ
1016:１３２人目の素数さん
20/04/15 10:45:06.91 5SCSS1OZ.net
仮に正しくてもそんなややこしい理論は必要ないんじゃないか？
誰も巻き込まれたくないw
1017:１３２人目の素数さん
20/04/15 10:53:10.19 b4Ht7CST.net
そらショルツは望月が何をやりたいかやりたかったか理解してるだろうその上での指摘だとおもわれる
1018:１３２人目の素数さん
20/04/15 10:59:05 5SCSS1OZ.net
これやっぱり駄目じゃないの？やり取り見た感じ
読み込んだが本当に理解不能って印象
1019:１３２人目の素数さん
20/04/15 11:00:37 5SCSS1OZ.net
↑ショルツが読み込んだが、ね
1020:１３２人目の素数さん
20/04/15 11:01:40 5SCSS1OZ.net
ま、頑張ってね京都の皆さん
1021:１３２人目の素数さん
20/04/15 11:11:08 lVWoKbS/.net
>>972
証明できていればややこしくてもなんの問題もない。
そもそも、簡単に証明できないから
ややこしくなっている。
1022:１３２人目の素数さん
20/04/15 11:19:36 r8DbtXP/.net
>>824
ＤＨＡを豊富に含んだ食品摂取で頭が良くなるって本当なんでしょうか?
最近話題になってたヨーロッパの天才児の食生活についても
「お魚を良く食べます」
ってお母様が仰ってました
1023:１３２人目の素数さん
20/04/15 12:15:15.85 upGWUHod.net
ブンゲン
「（数学的に正しいとは）水も漏らさぬ証明があること」「いかなる細部にも飛躍があってはならない」
よくぞ言った。
ブンゲン含め望月応援団は3.12→3.13の論証が、いかなる細部にも飛躍がない、
水も漏らさぬ証明であることを天下に示すべきである。
そのためには機械による検証が必要である。
それがないかぎりは、望月の証明は「数学的に正しい」とみとめられない。
1024:１３２人目の素数さん
20/04/15 12:15:47.31 upGWUHod.net
ごめん、3.11→3.12
1025:１３２人目の素数さん
20/04/15 12:57:01.17 QCk3Iyvt.net
Woitのブログ上で建設的な議論が進んでいるように見える
内容はわからないけど、とにかくややこしい問題だということだけはわかる
1026:１３２人目の素数さん
20/04/15 12:59:04.23 1rZ9apod.net
もう理解度と読み込みではIUTはショルツのもの。
1027:１３２人目の素数さん
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を用いたファイト・トンプソンの定理の機械的チェックの成功をアナウンスした
1028:１３２人目の素数さん
20/04/15 13:06:47 /g+JzMtk.net
>>983
＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？
Coqの正当性をCoqで検証すればいいんじゃね？
1029:１３２人目の素数さん
20/04/15 13:10:33 /g+JzMtk.net
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
URLﾘﾝｸ(ja.wikipedia.org)
1030:１３２人目の素数さん
20/04/15 13:13:18 QCk3Iyvt.net
>>985
そのプログラムの正当性はどうやって検証するの？
1031:１３２人目の素数さん
20/04/15 13:13:33 /g+JzMtk.net
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
URLﾘﾝｸ(ja.wikipedia.org)
1032:3%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C
1033:１３２人目の素数さん
20/04/15 13:15:03 /g+JzMtk.net
>>986
抽出されたプログラムにもう一度証明を食わせて
同じプログラムが抽出されればOK
1034:１３２人目の素数さん
20/04/15 13:16:45 LTi2Xsr9.net
>>988
インプットデータの正当性は？
1035:１３２人目の素数さん
20/04/15 13:22:26.67 LTi2Xsr9.net
>>987
カリー＝ハワード同型対応
は正しいが
Coqにそれが正しく実装されている保証がない
ゆえに、ふつうは二つの異なる証明系に食わせて、結果の一致までを見ることで精度上げることはよくやられる
１．もし、人間の証明と機械の証明結果が一致すれば、人の証明が正しい裏付けになる
２．もし、人間の証明と機械の証明結果が一致しない場合、人の証明が間違っている可能性が高いが、機械への入力ミスなどの可能捨てきれない
よって、人間の証明を、人が
再チェックして、確認することになるだろう
1036:１３２人目の素数さん
20/04/15 13:22:59.13 QCk3Iyvt.net
よくわかんないけどそのやり方で検証と言えるのかな
なんか正しいから正しいと言っているように見えるんだけど
1037:１３２人目の素数さん
20/04/15 13:25:21.63 /g+JzMtk.net
>>989
漫然とインプットデータといわれても困る
公理や定理の式が正しいとして、証明が間違っていたら？ということはない
公理や定理の式が間違っていたら？ それは検証系で検査できることではない
プログラム検証のV&Vで、
後のV(verification 検証)は機械的にできるが
前のV(varidation 妥当性確認）は機械で実施するものではない
URLﾘﾝｸ(www.ipa.go.jp)
1038:１３２人目の素数さん
20/04/15 13:26:31.69 LTi2Xsr9.net
>>990
> よって、人間の証明を、人が
>再チェックして、確認することになるだろう
だったら、状況はいまとあまり変わらないんじゃない？
Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
1039:１３２人目の素数さん
20/04/15 13:27:59.69 /g+JzMtk.net
>>992
誤 varidation
正 validation
1040:１３２人目の素数さん
20/04/15 13:29:04.99 LTi2Xsr9.net
>>993
＞Coqに食わせるのが簡単にできるなら、人のチェックと 平行してやればいいけど
たとえば、IUTの原稿ファイル貰って、それをCoqが機械読みしてくれなら簡単だが
もし、人が読んで、Coq入力を作るなら、それはすぐにはできないよね
1041:１３２人目の素数さん
20/04/15 13:30:09.19 /g+JzMtk.net
>>993
そもそも、理論として出来上がっているかどうかが疑問視されているなら
Coqへの実装は無意味ではないだろう
1042:１３２人目の素数さん
20/04/15 13:31:03.89 /g+JzMtk.net
>>995
もちろん、すぐにはできないが、やらない言い訳はないな
1043:１３２人目の素数さん
20/04/15 13:39:57 /g+JzMtk.net
>>990
Coqによる検証でも、人間によるテストを全部無くすことはできないが
「人間の証明を、人が再チェックして、確認する」
とかいう機械排除の口実は全く存在しない
1044:１３２人目の素数さん
20/04/15 14:26:02.19 upGWUHod.net
>>983->>998
のやり取りみるだけで、擁護派は数学的真理などどうでもよく、
機械検証をいわれたら逃げ回り、
ひたすら「望月がABC予想を証明した功績を認めろ」と強弁しているだけであることがわかる。
1045:１３２人目の素数さん
20/04/15 14:27:54.76 upGWUHod.net
それが結論
1046:1001
Over 1000 Thread.net
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 3日 5時間 15分 19秒
1047:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています