Interuniversal geometry とABC 予想60 



未だにcontroversialなIU幾何やABC予想に関する会話のサロンとして使って下さい。

荒らしはご遠慮願います

>>1

IUT応援スレと区別.混乱の防止のため、応援.信奉者の書き込みやこのスレのレスを応援スレへ引用は固く遠慮ねがいます 。
懐疑的な意見や関係者等の匿名の
論理的な擁護は歓迎です。

>>2

前スレ
Inter-universal geometry とABC 予想59

>>3

https://itest.5ch.io/rio2016/test/read.cgi/math/1762886294/l50

テンプレや資料は
前スレ Inter-universal geometry とABC 予想59などを参照下さい。

https://m.youtube.com/watch?v=2jgBBw6XjQ4&t=4264s&pp=2AGoIZACAQ%3D%3D

・Scholze-Stix（2018）は
「この図式を具体的に追うと、pilot objectのconcrete normalizationを入れると矛盾（または平凡化）する」
と具体的な反例・計算の道筋を示した。
・望月側は「それは単純化の誤り」と返すが、その「誤り」を避けた具体的な計算例・修正図式を第三者に見せられていない。
・Taylor Dupuyや一部のセミナー、Kirti Joshiの試みでも、
「ここで定義が曖昧で進められない」「Θ-pilotの扱いが追えない」
で詰まる報告が繰り返されている（2025年以降も進展報告なし）。
・2026年現在も
「具体的な楕円曲線（例：y² = x³ - x + 1 とか）で、Hodge theaterを1つ構築→Θ-link→log-link→不等式の数値評価」
のような最小限のtoy exampleすら公開・検証されたものがない。

>>6

共同通信記者からケドレヤへ最後の質問は良かった。

詳しい人が居ると面白いですね
もう1つのスレとは大違い
ところでlogが出てくるのは
別々にした積と和とを比較したいからなんですか？

LANAプロジェクトにフェセンコが参加してないのはどうしてなんだろ
ZMC副所長でIUT理解者のはずなのに不自然じゃないですか？
記者会見によればプロジェクト構成員は
コアメンバー５名＋学生やポスドクなどの若手メンバー７名
ってことだったけど

あえて望月ホルホルと見られてる輩は省いてる
スターだけは理論を理解するのにひとりは理解者が必要だろうとのことで入ってる
まあまあ望月と違って人もいいし丁寧に解説してくれるしな

>>11
加藤と星が入ってる時点でフェセンコだけ外す意味なくね？

>>12
加藤は一番理解してないのでカウントする必要ないな
フェセンコもまあ似たような理解だからな
役立たずのエセ理解者は最悪いらないけど、加藤はセンター長で、望月の腰巾着だから役目的にやらざるを得ない

>>7
>最小限のtoy example
そのレベルのことは論文執筆前の研究段階で嫌というほどやっててしかるべきなのに一つも出ないと
つまり実態を何一つ伴わない絵空事ってことか
ショルツェってめちゃくちゃナイスガイだね　そんな絵空事を邪険にせず絵空事と分るように説明してくれたんだから

>>13
>加藤は一番理解してない
ベストセラー書いたじゃん
あれで理解してないとかないわ

>>15
肝心の3.12のブラックボックスは正直わからんと言ってた
世間はそれを「理解した」とは言わん

伝え聞いた内部情報によると、LANA側は3.12の形式化を終えてギャップがあるという理解、は確定らしく、星を除く4名の結論は「限りなく誤り」
→しかし望月に聞いてもそれは違うの反応
→星が引き続き望月の手となり足となりLANA側に説明

7/17までに前向きな方向に行くのは難しいんじゃないの？

形式化ってもっとすごい時間が掛かるものかと思っていたけど、もうそんなに話が進んでいるのね。

>>17
デジャブで草
まんま8年前の望月とショルツェのやり取りじゃんｗ

>>19
ま、ショルツの2018年の論文はとある数論幾何の大家に「それは正しくない」と言われたみたいだから、ショルツが正しい、という当時の風潮は間違ってたことになってるのよね

> とある数論幾何の大家

誰ですか？
サイディならマッチポンプで利益相反
だ

・IUTTの「理解者」は基本的にこの世に望月新一提唱者しかいない。

➖➖
IUTTの検証.進捗情報の報告
2014年12月現在
京大数理解析研究所教授.望月新一

>それらのテーマ(絶対遠アーベル幾何」や 「エタール.テ-タ関数の剛性性質」 「Hode.Arakelov理論)精通している研究者は(私自身を除けば)この世に存在しないのが実情です。

> 関わっている 数名の研究者(サイディ.山下剛.星)を除けば、世界の 全ての数論幾何の研究者(=連続論文が公開された時点.2012年8月での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、での山下剛氏も含めて)はIUTの周辺にある数学に関しては「全くの素人」であり、これまでの研究業績の上に成り立っている「深い理解」を活用してIUTの成否に関する決定的な(=数学的に意味がある」)判定を下す資格が本質的にありません

>>21

https://www.kurims.kyoto-u.ac.jp/~motizuki/IUTeich%20Kenshou%20Houkoku%202014-12.pdf

>>17
MSはこの期に及んでまだ自分の誤りを認めない
しかし自分は表にでず星に説明させる
星はMSに逆らえないので板挟み

星　このままだと●うんじゃないかな？

天才レベル「鬼」：俺の理論が理解できない専門家は馬鹿
天才レベル「竜」：俺の理論が形式化できないLEANは無能
天才レベル「神」：俺の理論がフィットしないZFCは欠陥品

災害レベルやろ

>>21
ケドラヤだよ

ケドレヤはIUTの理解者でありません

>>20
その人が「正しくない」と言ったのが「正しい」？

>>27
いわゆるabc予想解決の3.12以外の部分のケドラヤの評価はポジティブだよ

>>28
検証チームが一年半議論してるからな、その結果は正しいんだろうよ、少なくとも外野の騒音よりはな

>>30
つまりその人が「正しくない」と入ったのはLANAの検証作業過程を経た上での見解だということ？

定理3.11から系3.12を導く論理について、LANAプロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じている

それ、ショルツェが8年前に言ったそのまんま

>>33
でもショルツの8年前のペーパーは正しいわけでなく、見解の相違がある

>>31
そうだよ

>>32
そうだね
でも検証の結果、ショルツも正しいとは言えないことも分かったようだよ

そんなこと書いてないよ

>>36
そのことはどこから分かりますか？もしや内部情報？

iut論文はnot even wrongで
誰でも一意に解釈できるようには書かれてない

s-sが主張したのはzfcの枠内で「彼らなりに」解釈すると
3.12を出せるほど強くないということ

同時に
別の解釈が成立したとしてどの可換図式が成り立つのか？
というchallengeを提案してる

だからs-sの解釈は誤解だって主張をするには
「ではiutを成立させる正しい解釈は何ですか？」に
答えられなければならない

woitのブログでもdupuyが
s-sの解釈は誤解で望月はそんなこと言ってない
ってscholze相手に食い下がってたが
scholzeの
では望月は何と言ってるんですか？
という肝心の問いに答えられなかった

さらに言えばs-s文書は
なぜiutが成立しないか
を説明したもので具体的なギャップを指摘したものではない
それに対してLANAが目指してるのは
具体的なギャップの有無を診断すること
だから目指してる場所が違う

>>38
331のLANA記者会見の議事録

>>39
SSの指摘は的外れという事実は確かで、それが正しい指摘だと喚いて乗っかっていた無関係の人々は恥を知れということ

かといって望月理論であることはが正しいともいえないわけだが、SSのあれが決定打というわけでもない

・キラン・ケドレヤ.Kiran Kedlaya。
望月新一ブログでNHKスペシャルの発言をダメ出しされた自称望月IUT信奉者Dupuyに近く、>IUTの周辺にある数学に関しては「全くの素人」かつ形式化も素人。

・望月新一認定IUT理解者(習熟)。　
2014年12月3名(サイディ.山下剛.星)
2020年2月IUT論文受理時でも10人未満。
IUTの研究普及(布教？)が主目的の次世代幾何学研究センター(望月新一センター長)関連のメンバーは
森重文.柏原正樹 .清水達郎
玉川安騎男 .望月拓郎..
Kedlayaもfesenkoも認定理解者
の枠の外らしい

よくわからない

なぜケドレヤがIUT検証のメンバーなの
か、よくわからない。
共同通信記者からケドレヤへ質問は
よかった

ケドラヤはこの一年半でIUTに習熟したらしい
ただし定理3.11から系3.12の飛躍はよくわからない（他の検証チームも同じ）
少なくとも外野の誰よりも数論幾何に詳しいし、IUTにも詳しい
そんな人の発言は重い

>>42
正しいかどうか判定して居た人は居ないでしょうよ
かなりの権威から指摘があったという事実だけで十分では？

SSの指摘は的外れなんて言ってないじゃん

>>41
３３１？

>>42 全く的外れではない

以下、数学が分かる人向け：
例えばjoshiに対する望月及びscholzeの批判は
（原理上）完全に正しいというわけにはいかないが
的を射ているという話
https://mathoverflow.net/a/468050

>>49
正しいから望月アウト、とも言ってないぜ

>>51
ケドラヤは「認識の違い」と言ってるぜ

そもそも認識の相違の余地がある数学論文がダメダメ

別の解釈が数学として成立すればs-sに批判を回避できる
s-sもその可能性を否定していない
ただ別の解釈が成立するというなら
それを説明しろ
どう成立するか示してみろ
と言っている

十数年たって今更なんか起こる蓋然性なんてほぼないと思うが
どのような結論が出ようが
iut論文が証明責任を果たしてない
ということはLANAプロジェクト会見でも再確認されている

>そもそも認識の相違の余地がある数学論文がダメダメ
その通り

だから not even wrong と評される

>>52
なんだ
正しくないなんて言ってないんだ

>>41
>LANA記者会見の議事録
公開されてるのそれ？

記者会見の議事録では、
記者からの質問が削除してある。

>>6

望月アウトとは言っていない、だからSSの指摘は的外れということなんだ！


？？？？？？

LANA記者会見とMの新年blogから分かったのは
LANAが躓いてるって箇所がMが素人である「基礎論」部分ってこと
対するMの言い分が「当たり前」や「専門家も認めている」だけじゃ
深刻なred flagと言えるんジャマイカ

「基礎論」部分への疑義は論文公表時からあったわけで
https://quomodocumque.wordpress.com/2012/09/03/mochizuki-on-abc/
https://inference-review.com/article/fukugen （"Model theorists"以下）
加えて「基礎論」部分こそが問題の核心だってS-Sの指摘もあったんだから
https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf
https://www.kurims.kyoto-u.ac.jp/~motizuki/Rpt2018.pdf （§4(T1), (T2)）
https://rio2016.5ch.io/test/read.cgi/math/1762886294/584-585
仮にLANAが更なるダメ出ししたところで
既に大勢が否定的な現状が再確認されるってだけで
（Mの態度に変化がない限り）
LEANがコミュツールとして役に立ったという評価にはならんじゃろ

ついでに
https://www.asahi.com/articles/ASTDB0C95TDBDIFI00WM.html
＞バザード氏は、ABC予想の証明は「誤り」と判定される可能性や、
＞作業量が膨大で検証が頓挫する可能性を上げている。もう一つの可能性は、
＞証明が「正しい」と検証されること。「そうなれば大きな驚きとなり、
＞数学界は望月氏に謝罪することになるでしょう」
こんときBは形式化プロジェクトが進行中って気づいてたんじゃね？
ってことは最後の発言はイギリス流の皮肉で真意は
「（結果次第で）望月氏は数学界に謝罪してくれるんですよね」
ってことかいな

数学板にも基礎論を軽視、ややもすると差別するような発言が見受けられるが、やっぱ基礎論は大事やねえ〜
ま、数学の基礎付けをする学問なんだから言うに及ばずか

ここはabc予想のスレだから、今の京都の現状を話せばそれで良いのではないか。

いやいや「基礎論」なんてフツーの数学者にはイランじゃろ
テンパって
＞いわば現代の数学では、禁じ手になってるようなことも取り入れて、
＞何かできないかということを考えたということなんですね
みたいなことを始めない限りは

桶は桶屋で良いんじゃね。
自分の生き残りのポストを掴む為に頑張れば、最低限良いのではないか。
数学者でない人がガヤガヤ言うものではないと思う。

みたいなことを始める基礎論音痴が多いのが現実

MSが公開したスライドを見たが、実際にできたのは
MS論文には書かれていないTh3.11.5からCor3.12を導く証明
Th3.11からTh3.11.5を導けるかどうかは現在奮闘中

あと、ZFCのLeanによる形式化云々のところで名前が出てくる
Shogo Saitoは、東北大学にいる数理論理学の研究者らしい

https://sites.google.com/view/sendai-logic/past-seminars/2024-4-2025-3

なお、3.11.5 (=3.11+Rmk. 3.9.5)　らしい

>>67
>MSが公開したスライド
どこにあるんですか？

>>69
https://www.kurims.kyoto-u.ac.jp/~motizuki/Formalization%20of%20IUT%20(2026-04).pdf

>>69
ありがとうございます
証明の正しさが検証されるまでもう少しですね

>>71
3.11.5⇒3.12はOKだとしても
3.11⇒3.11.5でNGと判明しそうな悪寒…

>>70
species/mutationの理論の射程が
＞independent of any particular model ZFC set theory!
とか強調してて、この人、完全性定理とか全く理解してないでしょ
（論文にZFCGがZFCの保存拡大だなんて書いてたくらいだから）
そんなもんはspecies/mutationとかのワケワカ独自理論でなく
圏と関手の枠組みで論じることが出来るはずです

＞ZFC as a first order theory
のくだりも何かものすごくヘンなことを考えてるでしょ
人間に無限を扱う能力があるみたいな
それは人類が１００年前に通り過ぎた場所ですよ
https://rio2016.5ch.io/test/read.cgi/math/1762886294/700

しかし
＞Ultimately, as a result of various consultations
＞with Lean experts, I reached the conclusion that
＞in fact the formalization of species/mutations
＞in the abstract using some sort of LeanForm of ZFC
＞as a first order theory (though ultimately theoretically
＞desirable at some possibly much later stage in
＞the project!) was most likely not necessary for
＞the LeanForm of (at least Stages 1∼2 of) IUT.
とメタ数学いらないかもとも言ってる（弱気になった？）

メタ数学が要らないでは無くて
lIUT全体をleanに落とし込む必要なしにleanに落とし込まれたZFCを使って種／変種を定式化できるだろう
といっているのでは？
つまり
この概念はIUT全体の成否にかかわらず
leanによって正しいと認められそうだと言いたいのかな？

ああその通り
species/mutations理論の形式化がいらないかも
って言ってるだけでした

>>72
そもそも3.11は正しいの？

From a purely technical point of view, the essence of LeanForm —atleast in the case of IUT — lies in undertaking a fundamental reorganization of the theory into suitable purely formal/combinatorial blackboxes
純粋に技術的視点から、Lean形式の核心は−少なくともIUTの場合−理論の、適切で純粋に形式的/組合せ的なブラックボックス群（数学の群ではなく”むれ”の意）への抜本的再編制を保証することの中にある

要するに「理論をブラックボックス群へ再編制することがLean形式化の核心だ」と言っている。
それは別に否定しないが、ブラックボックスはあくまでブラックボックスだから、最終ゴールである完全形式化に向けての（かなり手前の）中間ゴールだろと思う。
しかもその中間ゴールへの途上で早くも「超えられない壁」にブチ当たっている。
つまり「最終ゴールは遥か彼方にあって今の段階では目途の立て様が無い」という進捗ってことなんだろう。知らんけど。

>>77
やっぱleanによる形式化って
全数学を基礎から検証するようなものじゃなくて
ある程度の共通認識をブラックボックス化して
そこから形式的に導けるかだけ検証するってことか
これまでのライブラリってのも
全部そういうものなのかな？

だってブラックボックス群への再編制が完了したからって「そのブラックボックス達はそれぞれ本当に正しいの？」に答えられないじゃん

それともこれまでのライブラリってZFCから全部導出してるの？
最近気になってるのが
順序対(x,y)={{x},{x,y}}と定義していいのかとか
写像f:A→BをP(A×B)の部分集合とみなしていいのかとか
P(A)と2^A={f:A→2}を同一視していいのかとか
直和A+Bを(A∪B)×2の部分集合と見ていいのかとか
ZFCにおける「解釈」みたいなのはZFCの一部じゃないよなってこと
こういう「解釈」もleanに折り込んでるとすると
ZFCよりより武器が多いものになってないのかな？

>>79
だよねー

AIに聞いたら
・ブラックボックスは望月が初めて言い出した概念
・ブラックボックス無しの完全形式化が達成されない限り証明を検証したことにならない
だとさ
ま、そうだわな

>>78
>これまでのライブラリってのも
>全部そういうものなのかな？
AIいわく
ライブラリ＝検証済み
ブラックボックス＝未検証、つまり単なる仮定
理論のブラックボックス群への再編は一般的なLean検証では用いられない独自の方法論
とのこと

まあLean形式化はIUT論争を長引かせることが目的の確信犯的アクションなんじゃね？とも思えてしまう

>>84
なるほど

LEAN形式化の過程で幾つかの定理をブラックボックスとして
使うのは普通のことです
例えばBuzzardのFLT形式化プロジェクトでも1990年以前の結果で
形式化されてないものはブラックボックスとして使うと言っています
しかし今回のようにブラックボックスそのものに疑義がある場合
moduloブラックボックスの形式化にどのような意義があるのか不明です
>>70の文書のSkeletal Lean codeが何を示唆しているのか不明です
そもそも>>70の文書はmoduloブラックボックスで形式化するとも
言ってないのでこの議論自体無意味なのかもしれないよ

>>86
>1990年以前の結果で
>形式化されてないものはブラックボックスとして使う
全くダメじゃん
19世紀までの数学は全部検証して始めて意味がある

>>87
1990年以前の結果はwell-documentedだから
早晩AIで自動形式化できるようになるでしょう
詳しくはAITPMでBuzzard講演のスライドでも見てくださいな

ブラックボックス化自体が悪、とはいわない
何が証明されてないかが明確に意識されていれば構わない

今回、系3.12が”定理”3.11.5から導けたといってるから
証明されてない予想は、系3.12から”定理”3.11.5に移った

”定理”3.11から”定理”3.11.5は証明できるか？
なんともいえないが、今ここでつまってそうな感じがする

>>89
>”定理”3.11から”定理”3.11.5は証明できるか？
定理3.11が成立することは
誰もが合意できているんですかね？

>>90
>定理3.11が成立することは誰もが合意できているんですかね？
そんなこといってないよ

もし、”定理”3.11から”定理”3.11.5が証明できたら、
今度は証明されてない予想が、”定理”3.11.5から”定理”3.11に移る
それだけ

これをつづけていくことで、自明な前提まで遡れれば、証明の正しさが認められる

自明な前提がどこなのか？　さあ

LANAの人に聞いてくれ（笑）

ショルツの指摘はまあ普通に回答されるべき質問ではあるわな。
あれに変ないちゃもんつける方がどうかしてる

>>91
そんな手法でいいんですかね
上から引き下ろしていくんじゃなくて
下から積み上げていくのが数学でしょうに
IUTの最初からその正しさを検証していくのかと思ってました

上からでも下からでも完全に形式化された瞬間が証明完了。それまでは未完了。

そりゃそうですが
IUTは最初の方はあんまりおかしなところがないというのが共通認識なのかなあ
それとも
その辺におかしなところがあるなしにかかわらず
Th3.11→Th3.11.5→Cor3.12
が正しいと分かればあとはどうにか
よってたかってTh3.11の証明ができれば良いから
何とかなるんじゃないかという希望的観測も？

>>95
ねーよw
問題ない部分は部品パートだろ

系3.12が定理3.11.5から導けたって、アンタ、誇大広告でしょ
（実際、望月氏もそんなこと言ってないっすね）
望月氏はもともと定理3.11から系3.12が導けるって主張してるワケ
中間定理3.11.5を形式化して
そこから3.12が出ることを形式化したってんのなら
それなりにスゲーけど
望月氏の言う"Skeletal Lean code"ってナニ？
LEANの世界でもワケワカの独自用語でdiscommunication？

>望月氏の言う"Skeletal Lean code"ってナニ？
ブラックボックス間の論理的つながりをコード化したもの、つまり「こんなことを考えてるよ」を伝えるためのもの（as a communication tool）で、証明の検証からは程遠いもの
じゃね？　知らんけど

なにかと独自用語を持ち出すのは、要するに、検証としての進捗が皆無であることに対して鋭意推進中と言い訳するための言葉が必要だから

独自用語を持ち出さないと「進捗ゼロ」という報告にしかならないが、それだと予算取れない

といくら外野が吠えたって研究は粛々と進んでいくのだ
おまえらは指をくわえて見てるだけ～