Inter-universal geometryとABC予想(シン応援スレ) 92

前スレ：Inter-universal geometryとABC予想(シン応援スレ) 91
https://rio2016.5ch.io/test/read.cgi/math/1777882286/
詳しいテンプレは、下記旧スレへのリンク先ご参照
Inter-universal geometry と ABC予想 (応援スレ) 52
://rio2016.5ch.net/test/read.cgi/math/1613784152/1-13

（2030 ICM 日本開催に向け 力をためようということか）
https://www.mathunion.org/icm/icm-2026
ICM 2026
https://www.icm2026.org/event/ac193975-5d24-4628-8c30-ddb23de19a8b/catalog
Titles & Abstracts

https://ahgt.math.cnrs.fr/news/index.html
News of the AHGT project [Special year]2027-2028
Special year ``Arithmetic Homotopy Geometry'' at RIMS Kyoto, April 2027-March 2028.
Three Seasons: with main conferences, introductory lectures, and workshops

＜2026年は 数学でもAIの時代になるかもです。そういう兆候が2025年から顕著になっていますですｗ （＾＾； ＞
＜IUT最新文書＞
・News – Ivan Fesenko https://ivanfesenko.org/?page_id=80
・望月新一＠数理研 https://www.kurims.kyoto-u.ac.jp/~motizuki/
https://ja.wikipedia.org/wiki/%E5%AE%87%E5%AE%99%E9%9A%9B%E3%82%BF%E3%82%A4%E3%83%92%E3%83%9F%E3%83%A5%E3%83%A9%E3%83%BC%E7%90%86%E8%AB%96
宇宙際タイヒミュラー理論 ＜新展開＞ 2025年5月、中国の若手数学者の周忠鵬はフェルマーの最終定理の一般化がIUT理論から得られると発表した
・日仏遠アーベル共同研究 Arithmetic & Homotopic Galois Theory IRN https://ahgt.math.cnrs.fr/activities/
＜Grokipedia＞
Inter-universal Teichmüller theory https://grokipedia.com/page/Inter-universal_Teichm%C3%BCller_theory
遠アーベル幾何学 https://grokipedia.com/page/Anabelian_geometry
アーベル圏 abelian category Grokipedia https://grokipedia.com/page/Abelian_category

https://zen.ac.jp/lp/icp
IUT Challenger Prizeの紹介 2023年7月
審査の対象とする論文については、MathSciNetに載っていて、かつ、過去10年間に数論幾何の論文が10本以上掲載されている数学の専門誌に査読の上でアクセプトまたは掲載されたもの

://ahgt.math.cnrs.fr/activities/
Anabelian Geometry and Representations of Fundamental Groups. Oberwolfach workshop MFO-RIMS Sep. 29-Oct. 4, 2024
Org.: A. Cadoret, F. Pop, J. Stix, A.. Topaz （J. Stix IUT支持側へ）

://collas.perso.math.cnrs.fr/documents/Collas-Anabelian%20Arithmetic%20Geometry-IUT.pdf
“ANABELIAN ARITHMETIC GEOMETRY - A NEW GEOMETRY OF FORMS AND NUMBERS: Inter-universal Teichmüller theory or “beyond Grothendieck’s vision” Benjamin Collas Version 11/15/2023”

このスレの番号は前スレ43を継いでNo.44からの連番としています
（なお、このスレは本体IUTスレの43からの分裂スレですが、分裂したNo43スレの中では このスレ立ては最初だったのです！）
(余談)
Langlands program Geometric conjectures https://en.wikipedia.org/wiki/Langlands_program
つづく

>>577-578
数学シロウトか
はたまた ｗ大数学科初日オチコボレさんか
どちから知らないが
全く説得力ゼロだね

いいか
21世紀の現代数学 は、高度に専門化されているから
分野が違えば、他の分野の人は ことの成否は 正確には判断できないとしたものだ

なので、LANAプロジェクトの中間報告は Lean形式化未達だが
達成できる可能性はあると
そういう報告をした（今後1年かけるとかね）

ところで、今後1年は長い（長過ぎるのでは？）
話を秘密にする理由が希薄だと思うし
もっと、オープンな議論にした方がいいと思うな

そこで自然に
ダメならダメ
やれるならやれると
なると思うぞ

また無内容

ですね

http://810ch.net/test/read.cgi/inmu/1775396269/
http://script.s16.xrea.com/2ch/php/

http://810ch.net/test/read.cgi/inmu/1775396269/
http://script.s16.xrea.com/2ch/test/read.cgi/php/1469708255/

>>579
数学素人は自分だろ（笑）

＞中間報告は形式化未達だが達成できる可能性はあると

実際は、達成できないとまではいえない、という二重否定だがな

ニュアンスの違い　分かるか？　素人

証明できた　と　証明できないとまではいえない　の違い

＞今後1年は長い（長過ぎるのでは？）

●ねよ

＞話を秘密にする理由が希薄
＞もっと、オープンな議論にした方がいいと思うな

望月新一とかいう●違いにいえよ

＞ダメならダメ

ダメなんで諦めて●ね　ド素人
ガロア理論も分からん奴に数学は無理

>>579
>ところで、今後1年は長い（長過ぎるのでは？）
>話を秘密にする理由が希薄だと思うし
>もっと、オープンな議論にした方がいいと思うな

補足しておくと
下記 ”Arithmetic, Homotopy, and Geometry 2027-28”
が計画されている
下記の Scientific committee メンバーは、IUTに賛同し支持してきたメンバーだ
会議の内容は、IUT限定ではないだろうが
しかし、発表でIUTを是として引用文献に挙げることができるか
あるいは、IUTを非とする議論なのか？
それによって、発表内容が 当然異なる

”Season A - Apr-June, 2027”だから
今後1年 2027年7月にLANA報告だとすると遅い

なので、2027年7月にLANA報告を待たずに
議論をオープンにしないと、みんな困惑する
議論をオープンにすれば、その情報をベースにあとは各人が自己責任で考えることができる
状況は、悪いながらも それが最善だろう

https://ahgt.math.cnrs.fr/AHG-year_27-28/
Arithmetic, Homotopy, and Geometry 2027-28

Scientific Program & Seasons

Season A - Apr-June, 2027
Homotopy, rationality, and geometry

Season B - Sept-Nov, 2027
The homology-homotopy frontier in arithmetic geometry

Season C - Feb.-March, 2028
Combinatorial arithmetic geometry

Scientific committee: B. Collas° (RIMS Kyoto, JP), P. Dèbes (Lille, FR), B. Fresse (Lille, FR), Y. Hoshi (RIMS Kyoto, JP), M. Kim (ICMS Edinburgh, UK), A. Mézard (IMJ-PRG, FR) & A. Tamagawa (RIMS Kyoto, JP) - ° indicates lead.

また無内容

>>585
数学の論文が読めない素人には分からんだろうが
そもそもIUTはなかったものとしてすすめられている

だから、たんたんとIUTの"死亡宣告"を待てばよい

もどる
　>>242-245 より抜粋
ID:13yLpBZq さんの労作
(引用開始)
Claude Opus4.8とFable5使ってIUTを1から地道に検証するプロジェクトを個人的にこの一ヶ月やってみたがFable5の言い分は以下だった
IUT理解者に対する要請部分のみを書く

4. 要請
以下のいずれか一つをご教示いただきたい:
(A) 箇所の特定: (P) が(定義的措定ではなく)導出されている箇所 —— 論文・節・命題/Remark 番号 —— の特定。 すなわち、ラベル配置「テータ値 q^{j²} が j 成分に置かれる」から 受信側測度の主張「その可能な像の包が深さ ⌊j²·ord(q)−d−a⌋−b の領域に含まれ、 その体積が同じ正規化で q-標対象と比較可能である」への移行が遂行されている箇所。
(B) 機構の提示: (A) が「複数箇所の組合せから従う」場合、その組合せの明示 —— 各ステップが (i) 特定された構造の間の同型、(ii) 特定された正規化での体積計算、 (iii) 特定された領域の包含、のいずれかである形の命題列+証明の概略。
(C) 同値な別形: 実曲線(の無限族)に対する評価 L ≥ (l(l+1)/12 − 1)·|log(q)| の導出 (F3 により (P) の一様供給とこれは同値である)。

5. 予備的注記(想定される応答について)
略

6. 検証のコミットメント
(A)(B)(C) のいずれかが供給されれば、我々はそれを既存の形式化 (受け口となる構造は実装済み)に接続して機械検証することを約束する。
導出が成立すれば、検証結果は「Thm 3.11 ⟹ Cor 3.12 の連鎖は結論の独立な導出を含む」 —— すなわち望月理論側の確定 —— に翻り、その旨を同じ厳密さで記録する。
本要請は反駁ではなく、係争を機械検証可能な一点に絞り込んだ上での、 その一点についての情報提供の依頼である。

2. 論点の単離: ただ一つの入力
上記を全て投入すると、「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の連鎖の検証は、 次の一命題の導出に正確に還元される(これが我々の主定理群の内容である):

(P) [IUTchIV] Thm 1.10 証明 Step (v) において、Θ-標対象の可能な像の合併 (indeterminacies (Ind1), (Ind2), (Ind3) 込み)が、v_j ∈ V^bad の成分で λ := ord(q^{j²}) とした容器 φ(p^λ·(R_I)~) ⊆ p^{⌊λ−d_I−a_I⌋}·log_p(R_I^×) に含まれる —— ここで体積は、[IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f) で q-標対象の測定に用いられるものと同一の procession 正規化 mono-analytic 対数体積(受信側 (1,◦) の正規化)である
(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出である
(引用終り)

>>588 補足
これで
ID:13yLpBZq さん Claude Opus4.8とFable5使っての分析では
”「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の連鎖の検証は、 次の一命題の導出に正確に還元される(これが我々の主定理群の内容である):”
”(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出である”

１）要するに、「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」の部分が問題
　”(P) を認めれば以降は全て機械的に従う(検証済み)。問題は (P) 自身の導出”
２）なので、IUTのThm 3.11までは、OK
３）「Thm 3.11 ⟹ Cor 3.12 ⟹ 高さ不等式」で
”6. 検証のコミットメント
(A)(B)(C) のいずれかが供給されれば、我々はそれを既存の形式化 (受け口となる構造は実装済み)に接続して機械検証することを約束する。
導出が成立すれば、検証結果は「Thm 3.11 ⟹ Cor 3.12 の連鎖は結論の独立な導出を含む」 —— すなわち望月理論側の確定 —— に翻り、その旨を同じ厳密さで記録する。”

なので
>>588の(A)(B)(C) のいずれか を 提供せよ が、Claude Opus4.8とFable5からの結論だが
LANAの現時点での 結論はどうか？ そこの細部を オープンにした方が良いだろう
もう一つは、Leanコードの公開な
公開すれば、だれかがAI走らすかもしれんが、それはそれで仕方ない

(参考)
　>>339より再録
転載：ID:dythpcIC さん、ありがと
https://rio2016.5ch.io/test/read.cgi/math/1783860274/104-106
2026/07/17(金) 14:18:47.39 ID:dythpcIC
LANAプロジェクトに一定の敬意を払いつつも
逃げ腰でLEANの公開なしってのは流石にどうかと思ったから俺のOpus4.8とFable5で作った
プロトタイプ、スケルトン、未完成、言い方は何でも良いが公開しとくわ
コメントはほぼ日本語なんで海外勢向けではないがな
まぁAIに読み込ませてコメント英語化するとか容易だろうし許せ
https://github.com/Takkun-kohinata/IUT_LEAN
Opus4.8とFable5で作ったIUTの形式化

これからiutが数学者の議論の俎上に上がるとすれば、基礎論教育の必要性とか、leanのような形での証明の提出の義務化をどうするかとかでの過去事例とかで上がるくらいやろな

>>589 補足

念押し
”>>588の(A)(B)(C) のいずれか を 提供せよ”
の達成とか
その他
なんらかの形で IUTのギャップが
埋まる可能性は 大いにあると見ています （＾＾

「(P) [IUTchIV] Thm 1.10 証明 Step (v) において、
Θ-標対象の可能な像の合併 (indeterminacies (Ind1), (Ind2), (Ind3) 込み)が、
v_j ∈ V^bad の成分で λ := ord(q^{j²}) とした容器 φ(p^λ·(R_I)~) ⊆ p^{⌊λ−d_I−a_I⌋}·log_p(R_I^×) に含まれる ——
ここで体積は、[IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f) で q-標対象の測定に用いられるものと同一の
procession 正規化 mono-analytic 対数体積(受信側 (1,◦) の正規化)である」

(P)が証明できないので望月真一は死んだ

もう、10年以上前の2015年からここで止まってる

要するに2015年に既に死んでいる

2018年にはScholzeとStixにより具体的に指摘されている

要するに2018年に死亡宣告されている

こういうとき
やるべきことは一つで
決まっている
事実を冷静に見つめること
そのために、事実を隠さずに公開すること
みなで議論すること

事実を冷静に見つめた結果IUTは終わった

出すも何もlanaが出さないんだから議論のしようもないわな
このままなんも出なくて終わりやろな

最後には出るのでは？ソレが目的の1つでしたし

他責メンヘラおじさん望月

「ボクは悪くないも〜んみんながいじめる〜

ショルツが〜スティックスが〜

あいつらは学部レベルもわかってないバカです(キリッ」


↑情けないにも程があるだろw

他責メンヘラおじさん望月

「ボクは悪くないも〜んみんながいじめる〜

ショルツが〜スティックスが〜

あいつらは学部レベルもわかってないバカです(キリッ」


↑情けないにも程があるだろw

事実を冷静に見つめ
事実を隠さず公開し
みなで議論した結果
ＩＵＴ死す

>>595 追加
人生 ピンチはチャンスでもある
IUTは、ここを突破すれば、ひと皮むける 脱皮して 成虫になる
そう思って、がんばってください→望月先生たち
夜明けは近い

⚫︎2018年.

森重文京大教授のscholzeへ提案より数理研でscholze.stix.望月.星の4者ミーティング。

・個人的に、scholzeは"abc予想の証明へ近づく重要なアイデアは本当に見られなかった"と述べた。
quanta magazine 2018.9.20

⚫︎2019年.

1 望月新一。
川上量生が企画した望月新一監修加藤文元著IUT本刊行。

・本文　P37
>ワイルズの理論と望月教授の理論の違いは、、要するに言葉の違いです。
望月教授は、言うなれば、だれも 話したことがない、新しい言語を 用いて理論を組み立てました。
・本文　IUT語　p51
>IUT理論は、一般的な数学の パラダイムの枠内では語れない、
全く新しいフレームワークと言語・ 概念体系を基盤として構築されている

2 scholze。

>Scholze .Clausenは「凝縮集合」と名付けて研究を開始。
2019年4月、ショルツェはボン大学で「凝縮数学（condensed mathematics）」に関する講義を開始し、5月には77ページにわたるノートを公開した。
そのノートは、「コヒーレント双対性（coherent duality）」と呼ばれる重要な定理に対する、新しく洗練された証明へと結実していた。
後にショルツェと共同研究を行うヨハン・コメリンの回想「コヒーレント双対性については、それまでは極めて回りくどく技術的な証明しかなかった」。ショルツェとクラウセンの証明は、明快かつ優雅なものだった。
deepl
➖
condensed mathematics. condensed set

https://www.quantamagazine.org/two-researchers-are-rebuilding-mathematics-from-the-ground-up-20260520/

>>604 補足

下記の ＜文字起こし＞が面白い
１）加藤文元：一応その論文っていうのは自然言語で書かれてるわけじゃないですか
　それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
　で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね
　本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか
２）Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
　あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある
３）うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
　でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
　そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと

加藤文元さんの語り、面白い （＾＾

＜文字起こし＞より引用
1:04:52
（加藤文元）
あの、つまり、ま、一応その論文っていうのは自然言語で書かれてるわけじゃないですか。 はい。 で、ま、そこにか名があって、ま、どこまで完全理解できるかは別にして、ま、あの、その論文で、あの、なんか説明してるものありますよね。
1:05:05
うん。 で、それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ。 はい。はい。 で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね。本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか。
1:05:19
はい。 Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
1:05:26
あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある。
1:05:33
あー自然だから望月さんは自然言語で一応書かれてですね。数式と自然言語交えて書かれてわけですよね。
1:05:40
でそこをコンピューターで厳密なコードみたいな 形にする時に 表現できないものがある。うん。
1:05:47
それで間違ってるってことどう違う? だから本当に原理的にできないんだったら論理が飛んじゃってるわけですよ。
1:05:53
なのか 非常に難しくて理論として繋がってはいるんだけど
1:05:59
うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
1:06:12
そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
(引用終り)

埋めれるならとっくに埋めてる

そもそも望月論文は「証明の行間が空きすぎてわからない」んじゃなくてそもそも「基本的概念の定義が何言ってるかわからない」のが問題。それがわからなければ Lean に「証明のGapのありかをみつけさせる」なんてことも当然できない。だから「諸概念を第三者にきちんとわかるようにきっちり形式化してみせろ」と要求され続けてきた、で、現状やっぱりなという感じ。
もちろん Lean に乗せたコードをみればコードに乗せた本人がどう解釈したのかわかる。しかしそれがでてこない。まぁ出せんのやろ。LANAのメンバーですら、望月論文の諸概念をどのように形式化したらいいのかわかってないんやろ。「どうやって証明すればいいか」以前にそもそも「問題を数学の問題として形式化すらできない」の段階でつまづいてる。
なんとなく数学チックなそれっぽい文章でしかない。

形式化すらできない戯言を当然と思ってるのは
大学の微積と線形代数で落第した数学素人のSet Aだけ

論理が破綻してるんだから形式化なんてできなくて当然
最初から証明など無い

>人生 ピンチはチャンスでもある
>ここを突破すれば、ひと皮むける
>脱皮して 成虫になる
>そう思って、がんばってください
>夜明けは近い

脱皮できずに土の中で腐り●んだ
高卒素人がなんかいうとる

>>606-610
　>>607は、基礎論くんか お元気そうで何よりです。

>LANAのメンバーですら、望月論文の諸概念をどのように形式化したらいいのかわかってないんやろ。「どうやって証明すればいいか」以前にそもそも「問題を数学の問題として形式化すらできない」の段階でつまづいてる。

半分は正しいかもだが
半分以上ハズレではと思う

数学予想が しばしば山登りに例えられる
abc予想山 https://en.wikipedia.org/wiki/Abc_conjecture
山の頂は見えるが、途中は雲の中だ

望月論文 IUT I〜IV https://www.kurims.kyoto-u.ac.jp/~motizuki/papers-japanese.html
これを、山のステージ I〜IVと見る
各ステージ 1000ｍ級で
4000ｍ越えが IUT IV の ”Corollary 2.3. (Diophantine Inequalities)”P54
で、abc予想の山頂直結部分
Corollary 2.2. (Construction of Suitable Initial Θ-Data) P41
が、山頂直前

いま、問題にされているのは
ステージ IIIの
Theorem 3.11. (Multiradial Algorithms via LGP-Monoids/Frobenioids)P153
　↓
Corollary 3.12. (Log-volume Estimates for Θ-Pilot Objects) P173

ここの登山道で、Lean言語でもって道筋を示すマップを作ろうとすると
「なんか 繋がってないのでは？」となった
　>>605 加藤文元さんらの語り
”一応その論文っていうのは自然言語で書かれてるわけじゃないですか
　それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
　うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
　でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
　そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない”

まとめると
１）IUT以前は、abc予想山の登り方が、さっぱり分からなかったのだが
２）それにチャレンジした望月さんが、登山マップを自然言語で示した
３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
　3.11.→3.12.に見つかった（いまここ）

なので、
１）Lean語の方に何か追加するか
２）3.11.→3.12.の自然語記述を、もう少し緻密にするか
３）もっと以前から別登山ルートを探すか

私見ですが、１）or ２）で決着するのでは？ （＾＾

ある登山ルート上にどうしても通行できない箇所が1か所でもあればそのルート全体が無価値、登山したくば全く別のルートをゼロから探す必要がある
という当たり前のことがどうしても理解できないど素人さんだったとさ

望月のアイデアでは系3.12はどうやっても証明できない、したがってIUTそのものがゴミ
そのことを今から8年も前に正確に見抜いていたSS有能過ぎ
自明だー理解できないおまえが馬鹿なんだーとしか言えないM無能過ぎ

>>611 補足
>２）それにチャレンジした望月さんが、登山マップを自然言語で示した
>３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
>　3.11.→3.12.に見つかった（いまここ）

普通は、問題解決のタスクフォースを作る
その中で いまの場合、IUTとLean語の両方に詳しい人がほしいよね
望月氏や星さんは、Lean語さっぱだろう
なので、望月研の若手に Lean語を勉強させること
それから、ヤコビアン予想で活躍した AI Claudeなどを使う
タスクフォース作って、上記体制を整備すれば
自然言語→Lean語のギャップは 埋まるのでは？

ある程度タスクフォースでやってみて
早期に解決するなら それでよし

解決が長引きそうなら
正直に 全てをオープンにするのが良いだろう

世間で、多くの数学者が IUTを是として活動してきた
例えば、下記のRIMS 次世代幾何学国際センター 2022年4月とか
いろいろある
みんな、IUTのLean化は可能だと思ってきたはず

もし 解決が長引きそうなら
正直に 全てをオープンにするべし

(参考)
https://www.kurims.kyoto-u.ac.jp/ja/about-06-05.html
数理解析研究交流センター
次世代幾何学国際センター
広く次世代の幾何学の研究を推進し、新しい数学の国際的認知度向上のために研究成果を広く世界に向け情報発信するとともに、 国内外の若手研究者など多様な人材の育成を行うために、2022年4月に設置された。

>普通は、問題解決のタスクフォースを作る
問題の本質はIUTにABC予想を解くアイデアが何も無いこと
最善策はIUTを捨てること

「論文は理解できなかった。 自分の研究に時間を割くことにした。」
ファルティングス（望月の師匠）は最善策を取った。

>>611
＞１）Lean語の方に何か追加するか
新たな公理の追加はＮＧ
これわかんないやつは素人

＞２）3.11.→3.12.の自然語記述を、もう少し緻密にするか
この１０年できなかったことを
いまさらほざくのはド素人

＞私見ですが、１）or ２）で決着するのでは？
決着できなかった方法を
いつまでもいうのはド素人

ガロア理論も全く理解できなかった高卒素人が
利口ぶって数学板に書き込むな

ホイヨ
https://www.asahi.com/articles/ASV7W1QMDV7WUPQJ002M.html
正しさは誰が判断？　難問「ABC予想」論争が映す数学と社会
2026年7月29日朝日新聞
神里達博の月刊安心新聞+

　正しさをめぐる論争が、14年近く続く数学の証明がある。京都大学数理解析研究所の望月新一教授が2012年に公表した宇宙際タイヒミュラー理論(IUT)による「ABC予想」の証明だ。この予想は、いわば整数の世界における、足し算とかけ算の「奥深い関係」を表す根幹的な仮説であり、解決されれば多くの厄介な難問が一挙に解けるとされる。

　望月氏は16歳で米プリンストン大に入学した俊英。数論幾何――「数を図形に置き換えて考える」というホットな分野――で、すでに重要な業績を出していた。世界中の数学者が驚き、注目したのも当然である。

　ところが、その証明は合計500ページにも及び、斬新な概念や考え方が多数導入されていたため、理解できたとする数学者はごく少数にとどまった。同時に、批判を展開する数学者も現れた。影響が大きかったのは、ドイツの数学者ペーター・ショルツェ氏らによるものだ。ショルツェ氏は30歳で数学界のノーベル賞とも言われる「フィールズ賞」を受賞した、数学界の若きリーダーだ。彼は京都を訪れ、望月氏と直接議論したが、平行線をたどった。そして18年、IUTの定理3・11から系3・12を導く部分に深刻な問題があると指摘する報告書を公開した。

　一般に学術論文は、同分野の研究者による確認作業、「査読」を経る。数学論文の査読は長期化することもあるが、IUT論文は異例の7年半を要した。これを受けて有名な科学雑誌「Nature」は20年4月、「複数の専門家は、ショルツェ氏らの批判が出た時点で、この問題に決着がついたと見なしている」「論文誌への掲載が決まっても、それは変わらないだろう」と報じた。

　現状、IUTによるABC予想の証明を、世界の数学界は認めていない。だが「数学的に正しい」とは、結局どういうことなのか。数学者の多数決で決まるわけでもないだろう。望月氏の論文は学術誌の正式な査読を通過したのも、また事実である。事態は膠着（こうちゃく）状態に陥った。

　これに対し、打開策として始まったのが、定理証明支援システム「Lean」による検証プロジェクトである。証明をLeanに分かる言葉に書き換え(形式化)、論理の穴がないかを検査する試みである。

　プロジェクトチームは今月1…
この記事は有料記事です。残り1218文字有料会員になると続きをお読みいただけます。

https://researchmap.jp/kamisato
神里 達博
Tatsuhiro Kamisato
基本情報
所属千葉大学 大学院国際学術研究院 教授 (総合国際学位プログラム長)
学位
博士（工学）(2012年10月 東京大学)
修士（学術）(1998年3月 東京大学)
研究分野 1
人文・社会 / 科学社会学、科学技術史 /

こういう連中の喰いネタになったか

>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人

素人はおまえ
反例を列挙しよう

１）ZFCの前、"Zermelo set theory" https://en.wikipedia.org/wiki/Zermelo_set_theory
　では、公理はZFCと異なる形で与えられていた
　すなわち、ZFCにおいて加えられた公理も沢山あるよ
２）他に 有名な公理例で ”Grothendieck universe” https://en.wikipedia.org/wiki/Grothendieck_universe
　グロタンディーク宇宙公理 は、望月IUT IVでも特筆での解説があるよ

つまりは、一般凡人は、 新たな公理の追加はＮＧだが
しかし、数学天才には 新たな公理の追加は"G"なのだ
果たして、望月氏は 数学天才がどうか？ そこが問題だ by ハムレット

>>619
>こういう連中の喰いネタになったか

いまさら
前から IUTは
ドワンゴ 川上量生とタッグを組んでいる
ZEN大学の看板ネタ

まーだアホ朝日はシーソーゲーム演出してるのか
数学に対する見識がなにもないくせに
よく妄想だけでこんな恥ずかしいコタツ記事毎度書けるな

>正しさは誰が判断？
形式化できないものは誰が判断しても正しくない、というか数学ですらない
そんなことも分からないど素人が数学を語るな

>望月氏は16歳で米プリンストン大に入学した俊英。
しかしアラフィフで「自明だー、理解できないのはお前が馬鹿だからだー」と駄々をこねる子供おじさんになってしまった

>つまりは、一般凡人は、 新たな公理の追加はＮＧだが
>しかし、数学天才には 新たな公理の追加は"G"なのだ
じゃあSSに間違いを指摘されても人格攻撃しかできない凡人中の凡人はNGだね

>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人

下記のヒルベルト空間の例が合っているかどうか だが
有限次元の線形空間を Leanで扱えるようにはなっても
当然だが、無限次元は扱えない
だから、例えば 無限次元ヒルベルト空間を扱うための
Mathlib を整備すれば、その整備されたMathlibの範囲において
無限次元ヒルベルト空間が扱えるってことだね

これを、望月IUTにおいてみるに、まずIUT以外での
確立された遠アーベルMathlib の整備が必要だね

そして
その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
既存のMathlibで十分の射程内なのか
はたまた、既存のMathlibの射程外なのか
そういう議論も必要だってことだな

これからも議論は進んでいくだろう
それを見守る必要がある

(google検索)
数学 証明 Leanで 無限次元ヒルベルト空間は扱えますか？
AI による概要
Leanで無限次元ヒルベルト空間は十分に扱えます。公式数学ライブラリであるMathlibには、内積空間、バナッハ空間、およびヒルベルト空間（完全内積空間）の一般的な理論が定義されています。
https://arxiv.org/html/2602.17064v1
arXiv:2602.17064v1 [math.OC] 19 Feb 2026
Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

Leanにおけるヒルベルト空間の仕組み
・型クラス（Typeclass）による表現: 任意の型 \(H\) に対して「内積空間（Inner Product Space）」の構造と「完備性（CompleteSpace）」の性質を課すことで、次元の有限・無限を問わない抽象的なヒルベルト空間を記述します。
・具体的な無限次元空間: \(L^{2}\) 空間や二乗総和可能な実数/複素数の無限列空間（\(\ell ^{2}\) 空間、lp）などが定義されています。
略す

>>622
朝日とアエラだしひやっしー持ち上げてる奴らだし創価在日っしょ
笹川に言われてんじゃね

lean でヒルベルト空間が扱えるのかって
馬鹿だねえ

>>611
>１）Lean語の方に何か追加するか

アホらし

>>620
グロ宇宙はエレメンタリートポスでしかないだろ

>>626
>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない
>だから、例えば 無限次元ヒルベルト空間を扱うための
>Mathlib を整備すれば、その整備されたMathlibの範囲において
>無限次元ヒルベルト空間が扱えるってことだね
内容ゼロ

>これを、望月IUTにおいてみるに、まずIUT以外での
>確立された遠アーベルMathlib の整備が必要だね
関係無い。
系3.12（SS指摘部分）の形式化を目的に他部分を最大限ブラックボックス化したにもかかわらず大惨敗したのが今回の結果だから。

>そして
>その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
>上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
>既存のMathlibで十分の射程内なのか
>はたまた、既存のMathlibの射程外なのか
>そういう議論も必要だってことだな
それはIUTの完全な検証としてブラックボックスのホワイトボックス化で必要になる話。つまり系3.12が形式化できた後の話。
そこまで行く前に大惨敗だから関係無い。

>これからも議論は進んでいくだろう
>それを見守る必要がある
大惨敗で終了したのでいくら見守っても無駄。

>>630
>グロ宇宙はエレメンタリートポスでしかないだろ

アホらし
ちょっとあやしいが google AI下記でも
あと、グロタンディーク宇宙は その後のwikipediaご参照

(google検索)
エレメンタリートポスと グロタンディーク宇宙公理との関係は？
AI による概要 エレメンタリートポス（初等トポス）は、グロタンディーク・トポスを一般化・公理化した概念であり、すべてのグロタンディーク・トポスは初等トポスであるが、その逆は成り立たないという包含関係にあります。
概念の定義と包含関係
・グロタンディーク・トポス: サイト（一般化された位相空間）上の層の圏として定義される、幾何学的な動機に基づく空間の一般化
・エレメンタリートポス（初等トポス）: 集合の圏が持つ本質的な性質（有限極限、指数対象、部分対象分類子）を圏論的に公理化したもの。

宇宙論的背景（グロタンディーク宇宙との関係）
・巨大物の扱い: グロタンディークがトポスや圏を考える際、巨大な圏（すべての集合の圏など）を安全に扱うための前提としてグロタンディーク宇宙公理（到達不能基数）が利用される。

https://ja.wikipedia.org/wiki/%E3%82%B0%E3%83%AD%E3%82%BF%E3%83%B3%E3%83%87%E3%82%A3%E3%83%BC%E3%82%AF%E5%AE%87%E5%AE%99
グロタンディーク宇宙
グロタンディーク宇宙は、すべての数学が実行可能な集合を与える（実際には、集合論のためのモデルを与える）。

任意のグロタンディーク宇宙はある κ に対し u(κ) の形となる。これはグロタンディーク宇宙と強到達不能基数の間の別の同値性を与えるものである

>>631
>大惨敗で終了したのでいくら見守っても無駄。

？？？
ｗ大数学科入学で 初日の頭から冷や水あびせ 獅子谷落とし 授業で
震え上がって 即詰みになった おサルかい？ｗ　（＾＾

１）勝負は下駄を履くまで分らないという
　実際、加藤LANA発表も１年待てという
２）そもそも、数学は 勝った負けたの勝負ごとではない
　望月氏は IUTの成否に関わらず 数学の発展に寄与するべく 行動すること
３）それが最優先で、中途半端な誤魔化しは、よろしくない
　ダメならダメ、是なら是。是々非々をハッキリさせるべし

そうすれば、自然に道は開ける

ZFCに公理として追加するなら
V=L
だね
大変分かりやすい世界が広がる
ちょうど所謂ユークリッド幾何のようなものか
非ユークリッド幾何よろしく
V≠L
で考えるのも自由だが
V=L
をオーソドクスにすべきでないか

>>632
意味分かってないだろ

>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない

こんなあんぽんたんなこと平気でいっててつっかかってくる無能はなんなんや

>>636
カントール以前からタイムスリップだろう

>>634
>ZFCに公理として追加するなら
>V=L

かなり同意
L：ゲーデルの構成可能宇宙 https://en.wikipedia.org/wiki/Constructible_universe
（L is a standard inner model of ZFC、L is absolute and minimal）

が、もしかすると IUTには L＝Constructible_universe
は、狭すぎるかも

そこらも含めて
オープンな議論を希望します
そして、IUTの肯定的解決を望みます

>>636-637
話は真逆だよ

１）まず、下記 渕野昌先生「R. Dedekind の数学の基礎付け と集合論の公理化」見てね
　その中で、当時 Dedekindが、”無限の存在証明”を 真剣に考えていたとある
２）ところが、その後の公理系の研究が進むと、”無限集合”は「他の公理からの独立」と分った
３）これを いま 線形空間のLean化に当て嵌めると、
　有限次元の線形空間が扱えるライブラリーだけでは、無限次元線形空間は扱えない
　つまり、無限次元線形空間を扱うライブラリーを人が用意する必要があるということだ
（あたかも、”無限集合”の存在を 公理として与えなければ 公理体系として無限集合が扱えないのと同じ）
４）これを、IUTに見ると 従来の遠アーベルの理論のライブラリーだけで間に合うのか？
　それとも、さらに 望月IUTを扱う ライブラリーを 3.11に加える必要があるのか？
　そういう検討が必要になるということだ

まあ、加藤さんがいうように >>605「論文っていうのは自然言語で書かれてるわけ」
であって、あたかも Dedekindが”無限の存在証明”が 可能と思っていたが如くだ
”3.11→3.12 出来た！”と思っていたところ、あにはからんや それが自然言語のワナだったのかもね

まあ、そこらも含めて
オープンな議論をしていけば
ハッキリしてくるとおもう（＾＾

(参考)
https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1739-16.pdf
数理解析研究所講究録第1739巻 2011年 168-179
R. Dedekind の数学の基礎付け と集合論の公理化 渕野昌

P6
3 無限の存在証明
単純無限的体系によって自然数の全体の体系の基礎付けがなされうるためには，
そもそも無限集合の存在が大前提となる．しかも，これが，「数の理論を扱かう
論理学の部分の基礎付け」としてなされるためには，無限集合の存在が無条件
に証明できなくてはならない．
略
と書きながらも，晩年のDedekind が，無限の存在証明([3] の66.) の残った
ままのテキストをこの再版に回してしまったことの背景だったのではないだろ
うか．
ただし，Dedekind の名誉のために付け加えておくと，1911 年の時点では，
無限の存在が集合論の他の公理から独立であることは，当時の若い集合論の研
究者たちすら，まだ完全には把握しきれていなかった可能性がある．

無限公理(無限集合の存在を主張する公理) の集合論の他の公理からの独立
性は(集合論のすべての公理を含む体系の中で),
略
したものの組からなる構造を作ると，そこでは，無限公理以外の集
合論のすべてが成り立つことが確かめられ，そのことから「集合論
の公理系が無矛盾なら，集合論の公理系から無限公理を除いた体系
から無限公理は導かれない」ことが導かれる
として示すことができる．もちろん，[集合論の公理系が無矛盾なら」は，不完
全性定理以降の時代に生きる我々の後知恵であるが(9), Fraenkel が[7] で行なっ
ているような直観的な証明は，Dedekind の時代でも可能であったように思え
る．

応援でもなんでも好きにしたらいいとは思うが、せめてiutの何が問題でダメになったのかくらいは理解してからやろ

>>640
>応援でもなんでも好きにしたらいいとは思うが、せめてiutの何が問題でダメになったのかくらいは理解してからやろ

？
おれは、加藤さんや望月氏＆星氏に対して
LANA中間報告で
”iutの何が問題でダメになったのか”を
Lean コードを含めて 洗いざらいオープンにして
議論すべきと言っているのだが？

対して、加藤リーダーらは
概要と素人向けプレス記者会見はした
が、具体的なピンポイントの”何が問題でダメになったのか”は、
未公開だ

まあ、未公開→公開 には時間がかかるのかもね
あるいは、未公開で身内で検討して
「問題解決しました」の報告が出てくる可能性もある

>>641
時間がかかるんじゃなくて
隠蔽してるだけだよ

税金抜いてるIUTが

ど素人（ID:oyJUr6vp）がなんか言ってる
なぜそんなにバカ自慢したがるのか？

>>643
>ど素人（ID:oyJUr6vp）がなんか言ってる

ここには、プロ数学者は殆どいない
名誉教授が、巡回しているが
もし、君が 「自分は プロだ」と主張したいなら
それ証明してみｗｗ

私が見るところ
君は、ｗ大数学科に入学して 初日の冷や水を頭から浴びせる数学科洗礼で
ちんぷんかんぷん 目を白黒させて 高校までに持っていた数学イメージを壊された
オチコボレさんになった
ゆえに ４年でのゼミは情報系に逃げて 修士もそこの研究室で
情報系は、数理論理に近く 5ｃｈ数学板では 基礎論自慢

だが、一般の数学科の 特に代数系はサッパリ妖精だね
代数系壊滅で、iutの何が分るんだい？ 代数系ど素人のおっさんよｗｗｗ

(参考)
https://dic.nicovideo.jp/a/%E3%81%95%E3%81%A3%E3%81%B1%E3%82%8A%E5%A6%96%E7%B2%BE
nicovideo.jp
さっぱり妖精
魔法陣グルグルシリーズに登場するさっぱりな妖精である

>>642
>時間がかかるんじゃなくて
>隠蔽してるだけだよ
>税金抜いてるIUTが

意味わからん
それ言いがかりにすぎない

・「隠蔽してる」と主張するが、情報公開しないのは LANAの加藤文元氏だよ
　多分、意図は忖度と、情報公開したら 他の人たちと競争になって
　LANAプロジェクトとして面白くないってことかもね
・”税金抜いてる”は、妄想だね
　おクスリ飲もうねｗｗｗ

>>645
>おクスリ飲もうね

おまえがな　国粋高卒素人 Set A

>>644
>数学科の 特に代数系はサッパリ妖精だね

大学数学の実数と線形独立の定義が
サッパリ妖精の Set A がなんか吠えとる

>>645
文盲直せよw

IUT擁護派の書き込みって5chでもxでもそうだけど
主張とか文体からして
精神分裂とか言語障害が伺えるものばかりだよね

>>649
そもそも根本的に誇大妄想

>>646-650
夏だねー
虫が湧いている 暑いね

>>639
>３）これを いま 線形空間のLean化に当て嵌めると、
>　有限次元の線形空間が扱えるライブラリーだけでは、無限次元線形空間は扱えない
>　つまり、無限次元線形空間を扱うライブラリーを人が用意する必要があるということだ
線形代数もLeanも初歩の初歩から分かってないど素人の妄言

>>644
>だが、一般の数学科の 特に代数系はサッパリ妖精だね
群も環もイデアルもちんぷんかんぷんなど素人がなんかほざいとる

>>605 戻る
(引用開始)
下記の ＜文字起こし＞が面白い
１）加藤文元：一応その論文っていうのは自然言語で書かれてるわけじゃないですか
　それであの、それをあの、Leanに翻訳しなきゃいけないわけですよ
　で、あの、自然言語だったら、ま、なんとなく曖昧な部分でありますよね
　本当どう言ってるのかわからないで解釈不能な部分っていうのは許されるじゃないですか
２）Lean言語の時っていうのは解釈があの完全にこういう解釈だっていう風なことが分からないと
　あの書けないんですよ。 はい。 そうするとあの結局あの書けない部分がある
３）うん。 まだ分かってない。理解できてないからかけないだけなのかがそこが分からないのか。
　でもね、数学の論文って多かれ少なかれ やっぱりギャップはあるる。ギャップって必ずあるんです。
　そこ望月さんにそこ埋めてもらうしかないです。 ここがちょっと翻訳できない。望月さん、ちょっと
加藤文元さんの語り、面白い （＾＾
https://youtu.be/b6JlM_nrM3M?t=1
【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
ReHacQ−リハック−【公式】
166,727回視聴 2026/07/24
(引用終り)

１）まず、一般の理系では Leanに対する 自然言語の優位性がある
　つまり、自然言語は 赤ちゃんが、辞書（言葉の定義）も文法書（ルール）もなしで 母国語を習得する
　人間のディープラーニングだろう
２）自然言語では、厳密な語の定義なく 文法も厳密ではない。だが 分かり合える。人間だものｗ
　実は、数学以外の理系の学問では その方が良い
　というのは、数学以外の理系は 自然が相手で 自分が間違っていれば 実験と事実とかと合わないのですぐ分かる
　数学では、厳密性が尊重される（証明の有無が重要）ので事情が違うが、
　しかし 新しい数学を作っていくときには 自然言語による思考が適している
　なので、数学論文も数式や記号論理もあるが、その行間は自然言語で埋める。その方が圧倒的に読みやすい
３）が、たまに論文が難解すぎて「この証明大丈夫か？」と言われることがある
　そのとき、普通には 時間が経つと 別証明が出てきたりして、みんな納得するのだ
　なお過去にも、”コンピュータ証明をかけよう”というのはあった（有名なのが下記 フェイト・トンプソンの定理）
４）今回、IUT論文を コンピュータ証明にかけようと Lean化したが 途中で まだうまくいかないという 中間報告

取り敢えず、額面通り受け止めたらどうよ？
望月先生、がんばってください（＾＾

(参考)
https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A7%E3%82%A4%E3%83%88%E3%83%BB%E3%83%88%E3%83%B3%E3%83%97%E3%82%BD%E3%83%B3%E3%81%AE%E5%AE%9A%E7%90%86
フェイト・トンプソンの定理（奇数位数定理とも呼ばれる）
証明の改訂
完全に形式化された証明は、Rocq証明支援システムによって検証され、2012年9月にジョルジュ・ゴンティエ（英語版）とマイクロソフトリサーチおよびINRIAの研究者によって発表された[12]。

IUT擁護派必殺技でましたw
精神分裂コピペスレ流しw

キタキタ親父

>>654
高卒素人のいいわけが見苦しい（笑）

ギップルのふんどし

「多かれ少なかれギャップはある」

根幹で致命的なギャップあるの隠してるおじさんww

そもそも2015年以来指摘されてる肝腎の大ギャップが埋まらない
2つの計算がなぜ同値なのか全く説明できないまま

要するにただの妄想

>>654 補足
１）テンプレ >>13より
（SCHOLZE氏）
https://www.math.uni-bonn.de/people/scholze/WhyABCisStillaConjecture.pdf
Why abc is still a conjecture PETER SCHOLZE AND JAKOB STIX
Date: July 16, 2018.
ここの P10 “blurring”
"We voiced these concerns in this form at the end of the fourth day of discussions. On the fifth and final day, Mochizuki tried to explain to us why this is not a problem after all. In particular, he claimed that up to the “blurring” given by certain indeterminacies the diagram does commute; it seems to us that this statement means that the blurring must be by a factor of at least O( 2) rendering the inequality thus obtained useless."

２）用語“blurring”は、＜ケドラヤの発表＞ 動画
https://youtu.be/g0QLL8iYECY?t=2990 >>262
　にもあるし LANA中間報告書全文 >>327
https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf
P48
10.4. The effect of “blurring”.
にもあるが、
３つの不定性 Ind1, Ind2, and Ind3 と関連している
IUT III https://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20Teichmuller%20Theory%20III.pdf
ここが まさに Theorem3.11.で

３）私見だが、３つの不定性 Ind1, Ind2, and Ind3 や 用語“blurring”に関連する概念が
　いかにも自然言語であって そこが厳密なLean語に翻訳できない原因かもしれない・・

ともかく、まずは 望月氏たちのグループに頑張ってもらうしかないが
適当なところで、議論をオープンにした方が良いだろう
いまや IUT関連の遠アーベルの国際共同研究が走っているから
（まずは、内輪の遠アーベルのグループ内からとしても）

170 名前：１３２人目の素数さん[sage] 投稿日：2026/07/22(水) 14:54:20.14 ID:c+hkhx91
単関数て何？

>>662
可測かどうかで意見が割れているけれども。

>>661
＞３つの不定性 Ind1, Ind2, and Ind3 や
＞用語“blurring”に関連する概念が、
＞厳密なLean語に翻訳できない原因

根本からダメじゃん（切捨）

>>661
>望月氏たちのグループに頑張ってもらうしかない

10年以上同じところで立ち往生して
一歩も進んでないから全然ダメ

>議論をオープンにした方が良い

実は空っぽって暴露するのかい？（笑）

IUTは●にました

南無阿弥陀仏
アーメン

>>661
>LANA中間報告書全文 >>327
>https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf

＜補足(抜粋)＞
P49
10.5. Provisional assessment.
Of course, it should be noted here that there are also several points in common between our analysis and that of Scholze-Stix. Perhaps the most important common point is that both reports point out a problem in the “process of deriving Corollary 3.12 from Theorem 3.11,” and that this issue relates to the “identification of copies of the real number line R.” However, to elaborate further on the former point, although Scholze-Stix went on to
argue that “the suggested proof has [a problem] so severe that, in [their] opinion, minor modifications will not rescue the proof strategy,” we are not making any claims regarding the possibility or diffculty of remedying. Furthermore, regarding the question of whether a proof of the “abc Conjecture” exists, while many LANA members hold the view that “the original paper does not contain at least a formalizable proof,” the members were unable to reach complete consensus on this point.
(google訳)
10.5. 暫定的な評価。
もちろん、我々の分析とショルツェ・スティックス（Scholze-Stix）の分析との間には、いくつかの共通点があることにも留意すべきである。おそらく最も重要な共通点は、両報告書とも「定理3.11から系3.12を導出する過程」に問題を指摘しており、その問題が「実数直線Rのコピーの同一視」に関わるものであるという点であろう。しかし、前者の点についてさらに詳しく述べれば、ショルツェ・スティックスは「提示された証明には、彼らの見解によれば、些細な修正ではその証明戦略を救えないほど深刻な[問題]がある」と論じたのに対し、我々は、その修正の可能性や困難さについては何ら主張を行っていない。さらに、「abc予想」の証明が存在するか否かという点については、多くのLANAメンバーが「元の論文には、少なくとも形式化可能な証明は含まれていない」という見解を抱いているものの、メンバー間でこの点に関する完全な合意に至ることはできなかった。

SSに怪しまれました
確認したらやはり証明になってませんでした

完

>>667 追加
>while many LANA members hold the view that “the original paper does not contain at least a formalizable proof,” the members were unable to reach complete consensus on this point.
>さらに、「abc予想」の証明が存在するか否かという点については、多くのLANAメンバーが「元の論文には、少なくとも形式化可能な証明は含まれていない」という見解を抱いているものの、メンバー間でこの点に関する完全な合意に至ることはできなかった。

さて
・要するに、数学が議会のように 多数決で決まるならば、否決なのだろうが
・” the members were unable to reach complete consensus on this point.”は、加藤文元さんがガンバッたかもです
・ともかく、Leanに落とせない ←→ many LANA members hold the view that “the original paper does not contain at least a formalizable proof”
　なのでしょうね
・だが、LANA membersは 「何か足りないが、何かを足せば Lean化可能」と
　例えば、P49 10.5. Provisional assessment.
"On the other hand, our analysis does not give rise to this particular diagram; rather,
the elaboration of the η-algorithm shows that the proof of the final numerical inequality
hinges on the compatibility (9-1) which is not manifestly false. However, we, the LANA
project, do not have a proof of (9-1) at this time."
(google訳)
”一方、我々の解析からは当該の図式は導かれません。むしろ、η-アルゴリズムを詳細に検討すると、最終的な数値的不等式の証明は、明らかに誤りとは言えない整合性条件 (9-1) が成立するかどうかにかかっていることがわかります。しかしながら、LANAプロジェクトである我々は、現時点では (9-1) の証明を持っていません。”
より
これから、 (9-1) の証明を追加できれば OKとも読める
（これは一例）

まあ、ともかく 望月さんの側（単に一個人でなくグループで）が、何が問題なのかを きちんと把握して
対処するべし
それに尽きるのでは？

>・要するに、数学が議会のように 多数決で決まるならば、否決なのだろうが
証明が無いから否決
君、頭だいじょうぶ？

>「何か足りないが、何かを足せば Lean化可能」
abc予想は正しいという公理を足せばLean化可能

>>669追加
　>>611 より再録
数学予想が しばしば山登りに例えられる
abc予想山 https://en.wikipedia.org/wiki/Abc_conjecture
山の頂は見えるが、途中は雲の中だ
望月論文 IUT I〜IV https://www.kurims.kyoto-u.ac.jp/~motizuki/papers-japanese.html
これを、山のステージ I〜IVと見る
各ステージ 1000ｍ級で
4000ｍ越えが IUT IV の ”Corollary 2.3. (Diophantine Inequalities)”P54
で、abc予想の山頂直結部分
Corollary 2.2. (Construction of Suitable Initial Θ-Data) P41
が、山頂直前
いま、問題にされているのは
ステージ IIIの
Theorem 3.11. (Multiradial Algorithms via LGP-Monoids/Frobenioids)P153
　↓
Corollary 3.12. (Log-volume Estimates for Θ-Pilot Objects) P173
ここの登山道で、Lean言語でもって道筋を示すマップを作ろうとすると
「なんか 繋がってないのでは？」となった
まとめると
１）IUT以前は、abc予想山の登り方が、さっぱり分からなかったのだが
２）それにチャレンジした望月さんが、登山マップを自然言語で示した
３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
　3.11.→3.12.に見つかった（いまここ）
(引用終り)

１）4000ｍ越えのabc予想山に対して
２）望月IUTで、3000mのTheorem 3.11まで来た
３）その上に 望月IUTのベースキャンプ Corollary 3.12.が見える
　しかしLean言語でLANAプロジェクトが調べると ガケ崩れで 道が繋がっていない
　普通の数学者は登れないという
４）さてどうするか？
　一案は、Theorem 3.11→ Corollary 3.12.の Lean言語で繋がる道を作ること
　（ケドラヤ案は (9-1) >>669の証明を追加できれば OKだと）
　これが難しければ、Corollary 3.12.を移動し 変形するのもありだろう

はてさて、 望月グループは どうすべきか？
（個人的アドバイスは 望月研内で 若手Lean使いを育てること。また AIのClaude とかも(なんでも良いが) AI使いを育てることだな。若手の今後のギャリア形成にもなるし）
（金か？ 川上氏が金持ち。ZEN大との共同研究にする手もある）

>>671
ですねｗ

ABC予想の証明を山登りに例えるなら
IUTは頂上まで辿り着くはずだったルートが地図間違ってて、途中で行き止まりだったようなもんじゃないですか

>>674
でも登頂したってホラ吹いてる状態

ガロア理論の頂きを踏む

そもそも4実解も無理やんこんだけ騒動をヲチしてきたのにまだわかってない
そ頭が悪すぎる

>>671
>はてさて、 望月グループは どうすべきか？

・道は開ける。その強い信念を持って 取り組むべし
・数学史上でも しばしばある。自然言語の直感的命題が、後に厳密な証明が与えられることが
・有名どころでは、関数のフーリエ級数展開など（下記）

(参考)
https://en.wikipedia.org/wiki/Fourier_series
Fourier series
(google訳)
歴史
関連項目：フーリエ解析 § 歴史
フーリエ級数は、レオンハルト・オイラー、ジャン・ル・ロン・ダランベール、ダニエル・ベルヌーイによる予備調査の後、三角級数の研究に重要な貢献をしたジャン＝バティスト・ジョゼフ・フーリエ（1768–1830）にちなんで名付けられました。[ A ]フーリエは、金属板の熱方程式を解く目的でこの級数を導入し、1807 年にその初期結果を『固体における熱の伝播に関する覚書』 （Mémoire sur la propagation de la chaleur dans les corps solides）で発表し、1822 年に『熱の解析理論』 （Théorie analytique de la chaleur）を出版しました。この覚書では、フーリエ解析、特にフーリエ級数が導入されました。フーリエの研究により、任意の（最初は連続[ 3 ]、後に任意の区分的に滑らかな[ 4 ]）関数を三角級数で表すことができるという事実が確立されました。この偉大な発見の最初の発表は、1807年にフーリエがフランス学士院で行いました。[ 5 ]

現代の観点から見ると、フーリエの結果は、19世紀初頭には関数と積分の正確な概念がなかったため、やや形式的なものであった。後に、ペーター・グスタフ・ルジューヌ・ディリクレ[ 7 ]とベルンハルト・リーマン[ 8 ] [ 9 ] [ 10 ]は、フーリエの結果をより正確かつ形式的に表現した。