Inter-universal geometry と ABC予想 49

[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
上下前次 1-新

このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索歴削→次ｽﾚ栞削→次ｽﾚ過去ﾛｸﾞﾒﾆｭｰ

951: 2020/04/15(水)01:26 ID:zORjkTLC(1) AAS
ポストポスト構造主義の時代だ

952: 2020/04/15(水)01:35 ID:aU1czl6Y(2/2) AAS
>>950
すいませんでしたw　短く指示しようとしてしまって失敗しました。「ポストモダン批判の人」が適切ですね
個人的には（2）についての一種の留保が印象的でしたね。これこそまさにポストモダン的な部分で、
ある意味で複雑な問題なので
但し（2）の留保は一般的な話であって、基本的にはIUTに否定的ということでしょうが

953: 2020/04/15(水)01:51 ID:IyeZXVzi(2/4) AAS
君たちのレベルは分かったから
数学のＡＢＣを勉強しなさい

外部ﾘﾝｸ:www.chart.co.jp

外部ﾘﾝｸ:www.kyokashowork.jp

外部ﾘﾝｸ[php]:www.gakusan.com

954: 2020/04/15(水)01:54 ID:IyeZXVzi(3/4) AAS
君たちは上でも苦労すると思うけどもし習得できたらつぎはこれで勉強したらｗ

外部ﾘﾝｸ:www.chart.co.jp

955: 2020/04/15(水)02:01 ID:IyeZXVzi(4/4) AAS
**********ベールイ・タイプ議論*************

ふきだして眠れそうにありませんよ　暇なときに見てるんですね
そりゃベールイですね。いや同類。　3点抜いてる場合じゃないですね

956(1): 2020/04/15(水)02:19 ID:XXGhTXIb(1/2) AAS
擁護派が優勢になりつつあるのでは？
WはDavid Robertsの解説を読んで望月さんの視点に気が付いたようで、理解を示しつつありますね。
Dupuy,UF,Robertsの突っ込みに対しScholzeがまともに応える事ができるのか、それともお茶を濁して逃げるのかで、彼が数学者としての
誠実さを本当に持ち合わせているのかを見極められると思います。

957(1): 2020/04/15(水)02:36 ID:sDPcsM6G(1) AAS
>>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は最初から理解をしていたのだと思いますよ。

958: 2020/04/15(水)02:47 ID:GMXF0IZY(1) AAS
一般的な用語を勝手に違う解釈で使ったのならばアンドとオアを間違えてる方はどっちなんですかね

959: 2020/04/15(水)04:22 ID:PZKJ5Zxj(1) AAS
Wって誰？

960: 粋蕎 ◆C2UdlLHDRI 2020/04/15(水)05:36 ID:FI0JUvCQ(1) AAS
ヲイト氏の事とは違うん？

961: 2020/04/15(水)05:38 ID:xeYb99iT(1) AAS
Williamです

962: 2020/04/15(水)05:54 ID:38p90lrI(1) AAS
自分の考えを披露してショルツに考えてもらう感じだな
ショルツがそれなら可能性はあるかもしれないって言うか、全否定するか
ショルツにIUTを解いてもらう解決だな

963: 2020/04/15(水)06:05 ID:gAHsVD46(1) AAS
それもうショルツの定理だろ

964: 2020/04/15(水)07:38 ID:Rsdt7V/S(1) AAS
>>946
>S・Sはあっさり書いているが、当然望月氏も知っているはずだろうと思って書いていたはず。
>これは“Faltings’ theorem (Shafarevich conjecture) applied to the Weil restriction”した場合の話だよ。
>Finite Weil restriction of curves

レベルが高すぎて、すぐにはついていけないが
その話は、引用文献の下記のことかな？

外部ﾘﾝｸ:link.springer.com
省10

965: 2020/04/15(水)08:11 ID:XXGhTXIb(2/2) AAS
ショルツはAnabelian geometryの基本が全く理解できていないというDupuyのダメだしが炸裂しましたね。
>>957
>Wは最初から理解をしていたのだと思いますよ
なるほど、改めて読んでみたら流れを理解できました。

966: 2020/04/15(水)08:35 ID:TgZzPWYt(2/3) AAS
今ショルツが再び読み直してる感じなのか　どうなるのかな

967: 2020/04/15(水)08:47 ID:ZCZL7ADF(1) AAS
次スレ

Inter-universal geometry と ABC予想 50
2chｽﾚ:math

968: 2020/04/15(水)09:05 ID:WpCBiVcM(1) AAS
擁護派のコメントは望月本人のものでなければ、迷惑でしかないレベル

969: 2020/04/15(水)09:17 ID:Qr7I0O19(1) AAS
さいごはモッチーが勝ち、無冠の帝王になるにすーぱーもっちくん

970: 2020/04/15(水)09:31 ID:TgZzPWYt(3/3) AAS
ショルツは読み直してるのではなく、すでに相当理解していて、
擁護派のDupy氏が逆にショルツに質問、ショルツが解説している
（否定的に）ショルツの考えが変わる感じではなさそう

971: 2020/04/15(水)10:33 ID:+ag2Wthg(1) AAS
望月-ショルツの定理と呼ぶか
ショルツ-望月の定理と呼ぶかで100スレ消費
に10モッチ

972(1): 2020/04/15(水)10:45 ID:5SCSS1OZ(1/4) AAS
仮に正しくてもそんなややこしい理論は必要ないんじゃないか？
誰も巻き込まれたくないw

973: 2020/04/15(水)10:53 ID:b4Ht7CST(1) AAS
そらショルツは望月が何をやりたいかやりたかったか理解してるだろうその上での指摘だとおもわれる

974(1): 2020/04/15(水)10:59 ID:5SCSS1OZ(2/4) AAS
これやっぱり駄目じゃないの？やり取り見た感じ
読み込んだが本当に理解不能って印象

975: 2020/04/15(水)11:00 ID:5SCSS1OZ(3/4) AAS
↑ショルツが読み込んだが、ね

976: 2020/04/15(水)11:01 ID:5SCSS1OZ(4/4) AAS
ま、頑張ってね京都の皆さん

977: 2020/04/15(水)11:11 ID:lVWoKbS/(1) AAS
>>972
証明できていればややこしくてもなんの問題もない。
そもそも、簡単に証明できないから
ややこしくなっている。

978: 2020/04/15(水)11:19 ID:r8DbtXP/(1) AAS
>>824
ＤＨＡを豊富に含んだ食品摂取で頭が良くなるって本当なんでしょうか?
最近話題になってたヨーロッパの天才児の食生活についても
「お魚を良く食べます」
ってお母様が仰ってました

979(1): 2020/04/15(水)12:15 ID:upGWUHod(1/4) AAS
ブンゲン
「（数学的に正しいとは）水も漏らさぬ証明があること」「いかなる細部にも飛躍があってはならない」
よくぞ言った。
ブンゲン含め望月応援団は3.12→3.13の論証が、いかなる細部にも飛躍がない、
水も漏らさぬ証明であることを天下に示すべきである。
そのためには機械による検証が必要である。
それがないかぎりは、望月の証明は「数学的に正しい」とみとめられない。

980(1): 2020/04/15(水)12:15 ID:upGWUHod(2/4) AAS
ごめん、3.11→3.12

981: 2020/04/15(水)12:57 ID:QCk3Iyvt(1/3) AAS
Woitのブログ上で建設的な議論が進んでいるように見える
内容はわからないけど、とにかくややこしい問題だということだけはわかる

982: 2020/04/15(水)12:59 ID:1rZ9apod(1) AAS
もう理解度と読み込みではIUTはショルツのもの。

983(2): 2020/04/15(水)12:59 ID:LTi2Xsr9(1/5) AAS
>>979-980

１．有限単純群の分類で、2012年証明支援言語Coqを用いたファイト・トンプソンの定理(1963)の機械的チェックの成功をアナウンスした
　しかし、その他の大部分は機械的チェックなしなのです

２．1983 ゴーレンシュタインが、分類の証明が完了したとアナウンスした後、実は大穴が明いていることが判明(下記)
　
３．2004 アシュバッハーとスミス（ドイツ語版）が準薄群（すなわち偶数標数の体上の多くともランク2のリー型の群）について彼らの仕事を出版し、この時点で知られている分類の最後のギャップが埋められた

４．2008 原田とソロモンがマシュー群 M22（英語版）をカバーする、標準成分をもつ群についての分類の小さなギャップを埋めた。まあ、小さなピンホールがあったんだねｗ
省14

984(2): 2020/04/15(水)13:06 ID:/g+JzMtk(1/9) AAS
>>983
＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？

Coqの正当性をCoqで検証すればいいんじゃね？

985(1): 2020/04/15(水)13:10 ID:/g+JzMtk(2/9) AAS
>>984
具体的に説明するか

Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと

カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org

986(1): 2020/04/15(水)13:13 ID:QCk3Iyvt(2/3) AAS
>>985
そのプログラムの正当性はどうやって検証するの？

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.670s*