Interuniversal geometry とABC 予想61 



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

荒らしはご遠慮願います。

ZEN大学LANAプロジェクトの公式見解は中間報告書通りだが
加藤個人の見解はこうだよ

6月27日
Hodge-Arakelov理論の大域化によってabc予想が解けるかもしれないという病気にかかった人が、数学史上2人だけいた。1人はMochizukiで、もう1人がKimだ。

7月12日
いかに数学は論理の積み重ねだからといっても、時速300kmでセンチ単位の幅寄せするような運転し続けたら、プロだっていつか間違えます。

>>276
そしてこれはLANAプロジェクト代表として
どういう中間発表をすべきか腹を括ったという意味だろう
ギャップがあって形式化が無理だと表明すること
abc予想の証明になってないことを認めること

6月27日
昨日までエディンバラにいた。欧州は記録的熱波ということでエディンバラもスコットランドらしからぬ焼け付くような晴天だったが風は冷たく過ごしやすかった。Minhyong Kimの家でいろいろお話しした。私は何と戦っているのか、途中でわからなくなっていたが、最後にはまたわかって帰国した。

>>254
解かない可能性もある
数学で可能性をあーだこーだ言ってもしかたない
ってみんな言ってるんだけど、君、馬鹿？

>>275
加藤望月対話の根拠ね
加藤は対話という表現を一貫して使っているが
内容はギャップについての数学的な議論のはず

7月17日
本日の記者会見のまとめです：
我々の過去2年間にわたる取り組みの結論ですが、IUT論文において定理3.11から系3.12に至る論証のコンピューター形式化は現状では不可能です。しかし、この点に関する望月氏の追加説明が今も続いているため、現時点では最終的な判断を留保しています。

今回の記者会見でLANAが示した重要な成果の一つは、IUT理論における決定的な部分の論証について、IUTの専門家でない数学者たちが執筆した、一般の数学者にも理解しやすい長さの資料を提供したことです

(以下略

>>258
>まだアウトじゃない
加藤本人が解決には無限時間かかる（＝解決できない）かもしれないって言ってるんだから何の意味も無いんだよ

>>276
この等式の呟きもIUT理論によるabc予想でのミスの話だったわけだね
中間報告書を斜め読みする限りでは

7月7日
数学においてもっとも深遠でもっとも危険な概念は「等しい」ということだ。ふたつの抽象的構造を等号で結ぶことだ。

>>260
その通り。
今後の話は別の話。だって今後どうなるかは誰にも何も分かってないんだから。

>>264
星氏は理解者じゃないと？

>>264
>すごく役立ってるらしいっすよ
コミュニケーションツールとしてな　検証ツールとしてとは書かれてない

>>266
じゃ返事しなきゃよい

>>283
都合悪いから星を切り捨てたんじゃねw
IUT仕草ってやつww

>>264
gtrおじさんのダブスタ出ましたーー

>>275
対話で埋まるギャップならとっくに埋まってるやろ　望月は証明が正しいことを完全に理解してるはずなんだから
埋めるための対話じゃないのは明白

>>288
実際は加藤によるギャップがある事の説明と
望月による数学的釈明のはずだけど
まあ武士に情けではっきりとは書いてないわな
>>279で議論の目的ははっきり分かるけど

中間報告書は文章は望月寄りにして慰撫する意図があると思ってる
数学解説部分では嘘をついてないはずだが

>>280
はっ！
これは
史上初の
「無限の長さを持つ証明」
ではないのか？
ヒルベルトもゲーデルも間違っていた！？

この点に関する望月氏の追加説明が今も続いているため、現時点では最終的な判断を留保しています。

というのは事実上の白旗だけど立場上参ったと言えないだけ
こういうこと平気で言うからブンゲンも信用無し

パネルディスカッションにしてくれないかなあ
望月さんとleanチームやショルツスティクスとの対話
すぐには終わらないから無理か
でも延々やって貰っても良いんだけどね

望月が絶対に表に出ないから退職してからよ

一般に証明ができたという主張を批判する場合には、間違っていることを証明する必要はなくて、容易に埋まらないギャップの存在を指摘すれば十分です。

そういう意味でScholze-Stix 2018の指摘の価値を十分に認めた内容になっているように私には読めました。

「埋められる・・・
埋められるが・・・
いつ埋められるとは言っていない」
みたいな？

>>294
この報告と大筋で変わりないって書いてあるしね

>>295
カイジ乙

そもそも客観的に見て証明にギャップあるかもって論文が、ここまで相手にされてるのが変な話。無視されてもしょうがないと思うが。そんな話に血税を含む多額の資金•労力が投入されてきたこと自体が不誠実。リソースは有限である以上、それによって他の研究を進める機会が奪われていることが何より問題

はい！モッチーの証明は失敗でした！

今後もし証明のギャップを埋めるアイデアが（特にモッチーの示唆する方向で）見つかったとしても、それはそのアイデアを見つけた人の貢献ですね！

LANAプロジェクトは、モッチーのオリジナルの証明それ自体は失敗だったということをほぼ確認したように思います！

よし、とりあえず論文撤回しようね

なんかツイッターから批判的な論説をコピペして悦に入っている人がいるな

>>297
反論出来ないIUT擁護派おじさんの哀れなゴミレスで爆笑w
お前どこ卒だよマジでw

>>245
woitのblogならそもそもwoitと仲良いやつや捨てアド以外のまともな学術機関のメールアドレス開示するやつのコメしか承認されないだけだぞ
むかーし捨てアドだけど使えるメアドでふっつーのこと書いても承認されなかったしな

>>303
被害妄想くっそわらたw

じゃあredditはw

redditにもトピック立ったんだ
前見た時ないからみんな興味ないのかと思ってたわ
あと日本人は英語苦手だからじゃない？
見てみよ

>>306
URLは？

>>304
被害妄想なのか果たして、昨日またコメントしたけどダミーメアド使ったから公開されんかもね

>>307
r/mathにあるよURLくらい自分で探そ

>>309
出せないんですね
これじゃね？
https://www.reddit.com/r/math/comments/1uz6po8/latest_iut_formalization_news/

>>306
継続的に話題にはなってるよ
つまんないからすぐ終わるだけで

てかr/mathもコメント承認制か？コメントしたけど自分以外からは見えないわ
ブラウザ変えたら見えなくなった
そら擁護派のコメントとか見えんわけだわ

ブンゲンさんって日本語と英語で言ってることが微妙に違うよね
↓の英語では論文中に形式化可能な証明の記述がないことを
明言してるけど、日本語では「現状では不可能です」って
誰の責任か分からない曖昧な物言いになってる

それはそうとして、☆が詳細まで理解してるって設定は
どうなったんだよ

https://x.com/FumiharuKato/status/2078016732661424271
＞Fumiharu Kato 加藤文元（Bungen）
＞@FumiharuKato 4:19 PM · Jul 17, 2026
＞本日の記者会見のまとめです：
＞我々の過去2年間にわたる取り組みの結論ですが、IUT論文において
＞定理3.11から系3.12に至る論証のコンピューター形式化は現状では
＞不可能です。しかし、この点に関する望月氏の追加説明が今も
＞続いているため、現時点では最終的な判断を留保しています。
https://x.com/FumiharuKato/status/2078017230537892207
＞Fumiharu Kato 加藤文元（Bungen）
＞@FumiharuKato 4:21 PM · Jul 17, 2026
＞In today's press conference, we explained our efforts over
＞the last two years which resulted in the following conclusion:
＞The way the argument from Theorem 3.11 to Corollary 3.12 is
＞written in the IUT papers is unformalizable. But since
＞Mochizuki's explanation of this point has recently started
＞evolving, we reserve final judgement at this time.
【Google翻訳】本日の記者会見では、過去2年間の取り組みについて
説明し、以下の結論に至りました。IUT論文における定理3.11から
系3.12への議論の記述方法は形式化不可能である。しかしながら、
望月氏によるこの点に関する説明が最近になって進展し始めたため、
現時点では最終的な判断を保留する。

ブンゲンさん、LANA記者会見では、
S-Sの指摘とLANAの指摘したポイントは基本的に同じ、
しかし自分たちはより解像度が高い
って言ってるし（1:01:00〜ほか）、
S-Sを批難することは避けてるけど、
日本語の「仮想的質疑応答」では
https://note.com/katobungen/n/nbf629d03ad80
＞結論から申しますと、我々の報告とPeter Scholze氏および
＞Jakob Stix氏の報告の内容は本質的に異なっています。
＞そして、我々は彼らの誤謬を指摘することができます。
とか記者会見のときとは異なる立場を言ってる

redditって自動翻訳機能あったよな

>>312
もしかしてこれ？
With AI becoming increasingly capable of solving difficult problems, I've been wondering why LANA hasn't released its Lean formalization, even in an incomplete state. Even if the proofs themselves are unfinished, the definitions and overall formal framework would already be valuable to the community.

That's one of the reasons I decided to publish my own independent Lean formalization of IUT, developed with the help of Fable5. I also shared it on 4chan and 5ch in case anyone is interested in taking a look.

but, comment is japanese only.

https://github.com/Takkun-kohinata/IUT_LEAN

やってることは、論文に書かれていない後付けの解釈を望月が持ち出して、「SSの解釈は間違いでこちらが正しい」と言っているだけだからな。論文にはそんなこと書いてないのに。
しかも、その新しい解釈でも証明にギャップがあることには変わらない。

これでSSを「誤謬」とするのは酷い話だよ。

>>316
それだよ
やっと承認されたか
woitの方にも似たこと書いたけど承認されんわ

>>313>>314
英語の方が本音です

>>318
多分本人がやってるから時間かかってるだけじゃんないかな

てか誰かも言ってたが、トートロジー的閉ループを構成する証明ってたぶんLEANは向いてないよな
キュービカルAgdaとかでHoTT使わないと計算できないってLEANやってるとわりと色々なAIが言う話だ
俺の独自物理理論もそれだし、IUTもどうやらそれだと今回はっきりしたろ
問題はキュービカルAgdaにはmathlibがないことだろうけどね

LEANにHoTT導入するならunivalenceはどう足掻いても公理化するしかないからその部分は計算不可だし
LEANをcubical Agdaに変換するAIが求められるな

ホモトピー型理論は既にLeanにもライブラリがある

>>312
>そら擁護派のコメントとか見えんわけだわ
擁護派そのものじゃないかもしれないが
ショルツスティクスさんの間違いを指摘できるというコメントは読めるけどね

>>322
そら公式ではないけどモジュールはあるよ
LEAN4のカーネルの一位性証明とHoTTのunivalenceは本質的に矛盾するから公理化して計算不能にするしか無いんじゃないの？複数のAIの受け売りだから間違ってるかもしれんが

十数年正しいって思い込み続けてたものが
無意味で荒唐無稽なゴミだったって自覚したら自殺するのかな尊師は

自覚あるけど沈黙して終わり
数十年後の数学史にどう名が残るか
ブンゲンもそうだけどね

指摘を受けた時点で問題点は認識していたと思う。でも、IUTを前提にキャリアを積んできた弟子達のために、撤回という選択肢を取れなかったのでは。

ずば抜けた存在と一旦認められてしまえば
そのあとでごみ論文を書いたとしても
名は残る

>>321
>俺の独自物理理論

具体的には何ですか？
加藤文元がいう望月新一語で書かれた
全く新しい数学のIUTはトンデモですが、これと同類ですか？

トンデモを精密化しても出力は
ガラクタのトンデモ

まぁyoutubeとかで「俺lean使える」とか言ってるやつは「何故leanで証明の検証ができるのか？そもそも証明とは何か？」という基礎論レベルからちゃんと勉強して理解できてるわけじゃないからな
なんとなくインストールしてカタカタやってるうちに使い方だけ覚えたで終わってるだけだから「leanで何ができてるのか」なんてまるで分かってない

いつも通り、IUT理論が間違っていると結論づけた愚か者たちは事実関係を歪めるのに忙しい😂🤣 reddit.com/r/math/comment…

IUTGtr@IUTTOfSM19697月18日(土) 11:09

>>312
どういう書き込みしようとしたのか見てやるよ
どーせここと同じで文にすらなってない気狂いのお前がクソ漏らしてんだろww

プーアノンっぽいアイコンで爆笑w

>>316
LLM英語丸出し
そしてすでに証明したとかいうキチガイ言及はできず

ビビリキチガイw

>>321
数学に向いてないんよ
数学になってないゴミだから

>>312
ほんと短絡的なキチガイ妄想で生きてんだな
生まれつきなのか？それ

望月が言う「ショルツェの simplification」とは、本来標準的な数学の言葉へ翻訳不可能なIUT語を無理やり翻訳した結果、IUT理論を縮退させてしまっていることを指している。
そして「異なる方法で得られる2つの対数的体積（実数の物差し）を同一視してよいか」の問題（今回加藤が非常に難しいと語ったもの）の回避がIUT語の設計段階からビルトインされているから自明に同一視可能と主張している。
しかし形式化できない理論はそもそも数学とは呼べないからそのような主張もまったく無意味となる。今回のLANAプロジェクト報告はその可能性を従来よりも強く示唆している。

>>327
お優しいですね

>>328
アチャ～

望月怪文書も出ないしもう白旗あげたんだな
文元にも梯子外されてブルータス、お前もか状態w

アホのmathjinがまたご都合解釈でショルツスティックスを悪者にしてキャーキャー騒いでるけど現実はこう

黒木玄 Gen Kuroki
@genkuroki
·
21時間
返信先:
@genkuroki
さん
#数楽 一般に証明ができたという主張を批判する場合には、間違っていることを証明する必要はなくて、容易に埋まらないギャップの存在を指摘すれば十分です。

そういう意味でScholze-Stix 2018の指摘の価値を十分に認めた内容になっているように私には読めました

>>326
少なくとも日本の数学史の汚点としては確実に残る。

まあ一族郎党末代までの恥だよな
あれだけ自明自明ってゴネ続けて批判者にハラスメントしまくってたのに
その結論が8年前のSSレポートの通りでした！だもんなぁw

>>339
関連スレにいるキチガイAIおじさんとmathjinしか味方がいないw

IUT擁護派おじさんが発狂コピペしててワラタw


【数学】「ＡＢＣ予想」巡る望月新一教授の証明、検証チーム「不明瞭な点がある」と中間報告 [すらいむ★]
https://egg.5ch.io/test/read.cgi/scienceplus/1784298129/

ショルツェに後れをとってしまったようだね？

>>327
望月はあっちなんか嫌なことあったんでしょ
日本は京大は研究に最適ってこと何度も繰り返し言ってるから
また始まったと思ったんじゃないのかな
あっちは変な奴が論争吹っかけてくるからw

>>324
何いってんだか
君はまさか新しいロジックだとでも思ってるわけなのか

>>347
ID:joumQYeu
そのIUT擁護派おじさんはLLMコピペしてるだけなので、、、
LLM使おうにも基礎ができてないとピエロなだけっていうのを教えてくれるサンプルですね

>>347
新しいロジック？？どう言う意味？

ブログで法の支配とか適正手続を強調してたんだから一応適正手続が保障されて納得はしてるんちゃうの

IUT擁護派おじさんついにバックレるの巻

👇

157 名無しのひみつ 2026/07/20(月) 20:08:24.06 ID:jDVnUfx7
そもそも査読は、論文としての体裁が整ってるかどうかって判定にしか機能してねー、どころか、体裁が整ってても査読者の気に入らない
結果だと、屁理屈つけられて落ちる

ってか、査読システムが全く機能してねーのに、査読論文数とか被引用数で研究業績評価するから、世の中は屑論文であふれてるわけな
https://egg.5ch.io/test/read.cgi/scienceplus/1784298129/157

理解してないのに何か擁護できると思っているのは不可思議ですね

そりゃそう思うわな LEAN でできることできないことが全くわかってないんやろ
LEAN で形式化できないならもうそんなもん数学の論文でもなんでもないというのがわかってない
そのレベルのあんぽんたんなのにわけもわからずでかい口たたいてんだからたたかれて当然やわな

問．次の三者の意見から仲間外れを探しなさい

Scholze ＠ Woitブログ
>As I said, it's very easy to convince me that (2) is wrong:
>Just point to one diagram whose commutativity is rescued by
>allowing this indeterminate isomorphism of π_1(X)'s
【訳】既に述べたように、(2)【注：同型コピーは不要という主張】が
間違っていることを私に納得させるのは非常に簡単です。
π_1(X)のこのような不定な同型を許容することで可換性が助かる
図式を１つでも示せばよいのです。

LANA ＠ https://www.youtube.com/watch?v=KADN5NHmIfw　50:00〜
等式「η_q = η^anab_S」を満たす S さえ見つかれば
S-Sが考察しなかった非自明な可換図式が出て、3.12が証明できる

望月 ＠ IUT論文III
そんな等式は"tautological"な理由により成り立つ

LANAが「壁」（普通の言葉では「ギャップ」）と呼ぶものが
望月にとってはtautologyである理由はたぶん
LANAが避けたspecies/mutationsの理論に
ミソがあるからなんじゃないか

しばらくしたらご託宣がある？

species/mutationsの理論は形式化できないから
実はミソじゃない方なのかも知らんけど

MathlibにZFC形式化を実装させればspecies/mutationの形式化はできるんじゃないの？
それができれば、解決に近づく

>>356
>species/mutation
て何？

IUTが形式化できなければ
>そんな等式は"tautological"な理由により成り立つ
は数学の主張ではなくただのお気持ち表明。
さあ困ったね望月さん。

RIMSもIUTの形式化に取り組んでるらしいね
LANAが形式化に失敗してRIMSが形式化に成功したと言って対立したら面白い

>>356
ZFCのライブラリはあるし
中間報告書もそんな事は問題にしてない

普通にleanの公式documentにある。
そもそもleanは可算無限階層の集合論までまんまで形式化できる。
ZFCの分出公理を形式化をもとめても2階くらいですむ。
lean の能力で形式化できないような数学ならそんなもの元々無矛盾性の担保をどうするかの問題もでる。Lean に実装してるレベルならふつうの ZFC 内部に Forcing できるので問題にならない(Lean の体系が矛盾してるならそもそもZFCが矛盾してるわけだからLeanがどうこうの話でなくなるから)
大体そもそも今回の報告で「Leanの表現力ではIUTを形式化できなかった」なんて話だれもいってない。「俺たちの思う形式化はできた、でもそれだと証明は完成してなかった」という話。
もちろんその「俺たちの思う形式化」がまちがってて望月先生のそれとはずれてるという言い訳はできるわけだが。
結局「LANAの形式化」があってるなら証明にはあながあったって話になるし、間違ってるというならじゃあ正しい形式化はなんやねんとなる。もちろんこれは望月先生ご本人がなんかコメントだすしかないわけだが、まぁもうでてこんやろ
だいたいその「LANAの形式化」が発表のなかにはいってないんだからそれもほんまにつくってみたのかどうなのかまったくわからん。
せめて「LANAの形式化」をちゃんと発表するのが筋やろ。給料分の成果みせろっちゅねん

まあその通りだけど
基礎論向こうで言うところのLogicが分からん人には通じないかと
望月のやってるような凄く新しい数学も
凄く狭い範囲内ですごく複雑なことをやってる
と基礎論の立場からは言える事をわかってない
既存のLogicの枠に収まらない数学だと思ってしまっている

致命的なギャップを聞く耳持たずで自明自明言い張り続け
指摘者に圧力かけまくり誹謗中傷しまくりだった恥ずかしい老害、leanでトドメを刺されて死亡

species/mutation

普通の数学では

* 群
* 環
* スキーム

などは「対象(object)」として扱います。

そして

* 準同型
* 写像
* 関手(functor)

を考えます。

つまり

> **対象 → 写像**

という世界です。

しかしIUTではこれでは足りません。

IUTでは

> 「アルゴリズム」

そのものが重要になります。

例えば

```
あるHodge theater
↓
Theta-link
↓
別のHodge theater
```

これは単なる写像ではありません。

「こういう情報だけ取り出し、

こう加工し、

最後にこういう情報を忘れる」

というアルゴリズムになっています。

望月氏は

これを

**mutation**

と呼びます。

speciesは

> "ある種の数学的対象"

です。

例えば

* group
* ring
* scheme
* diagram

など。

しかし重要なのは

speciesは

**「集合として定義される」のではなく**

**"定義そのもの"**

として扱う点です。

つまり

普通なら

```
G = この群
```

ですが、

speciesでは

```
Groupという型
```

を扱います。

Leanで言えば

```
Type
```

に近い考え方です。

mutationは

speciesからspeciesへの

**アルゴリズム**

です。

例えば

```
Ring
↓

Monoid
```

なら

```
掛け算だけ取り出す
```

というアルゴリズムになります。

あるいは

```
Elliptic Curve
↓

Theta-data
```

という変換もmutationになります。

つまり

```
入力

↓

決まった処理

↓

出力
```

というもの。

---

望月氏は

mutationは

実質

**functorial algorithm**

であると言っています。

普通の圏論では

```
Category

↓

Functor

↓

Category
```

です。

しかしIUTでは

「どのデータを保持し

どのデータを忘れ

どのデータを曖昧にするか」

が非常に重要になります。

例えば

```
Ring

↓

Multiplicative Monoid
```

では

加法を完全に忘れています。

IUTでは

こういう

「情報を忘れる」

操作が何十回も出てきます。

そこで

mutationという概念を導入した方が

論理が整理できます。

謙虚さも忘れてしまったのか

何上からしゃべってんの？
圏論も基礎論も計算論もなにもかも真面目に勉強したことないやろ？
そんな態度でなんかしゃべる資格自分にあると思ってんの？
あほか

LANAは中立でもなんでもなく、Zen大学でIUTの講義をやってたり
ブンゲンさんがIUTで稼いでたりしててもろ利害関係者なわけよ

だから、宇宙際まで旅したけどABC予想の証明の最後の１マイルだけ
道が通ってなかったってストーリーがLANAに許容できる限界なわけ

実はIUTは意味のないガラクタを寄せ集めた伽藍堂でした
みたいな結論には絶対にならない

LANAが表立ってIUTの根幹（species/mutations）まで
突っ込まないのはたぶんそのせい
（望月新年日記によれば内内でのやり取りはあったはず）

狂信者にとってみれば
形式化できないのは不信心者がIUTのエッセンスを拒絶してるから
ってことになるんでしょうけど

IUT賛同派が母体のLANAですら
「論文中に（形式化可能なｗ）証明がない」
ってことを認めざるを得なかったのは
部外者を中核メンバー入れたからなわけだけど
これはIUTビジネスのスポンサー（かわんご）の意向でしょう

かわんごがいなかったらと思うと彼は結構良いことをしたよね。まあ界隈外の数学者にとってはとっくに意味をなくしていたのだろうから、日本村の解体への貢献だが