Interuniversal geometry とABC 予想61 



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

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

ホモトピー型理論は既に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ビジネスのスポンサー（かわんご）の意向でしょう

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

まあさすがに最後の理性は残ってたってところだな。LEANの出力内容を誤魔化すってことだけは流石にできなかった。
あのグループにできる最後の言い訳がショルツも正しくないっていちゃもんつけるってところだけだったってことだわ。

「3.11 = 3.12」 を分解して形式化をはじめている

前半 (3.11)
APT (アルゴリズム的並行移動)
IPL (入力整合性)
→第1~第3三角形

後半 (3.11.5= 3.12)
SHE (同時正則表現可能性)
IPL (input prime-strip link)
→第4三角形 (現在RIMSが形式化に取り組んでいる箇所)

>>374
加藤は望月の盟友みたいなもんだぞ
望月がIUT理論考えてる時のブレインストーミング相手なんだから
だからあんな優しい中間報告書に留まってるのに
お前は人でなしだな

>>376
LANAプロジェクトなければabc予想証明失敗は有耶無耶になっていたと思うからZEN大学の数学への貢献だわな
プロジェクトチームに人呼ぶにも金がかかるからな

4つの三角形について
この理論は4つのステップに分かれる
・第1三角形
入力:BPS
出カ:マルチラジアル表現
→「0列」との貼り合わせとして理解できる
・第2三角形(下降 dsc)
情報を簡略化する
完全なデータ→群論的部分だけへ
・第3三角形 (HDD)
dsc の結果に対して
hull + determinant 操作を適用
・第4三角形 (SHE)
特別な入力(qパイロット)に制限

今回のLeanコードの対象:
第4三角形のみ

lUTのLean形式化は、次の段階に分けて進める

・Stage1
[IUTchlll] 定理3.11=系3.12
・Stage2
[UTchll]定理3.11の証明
・Stage3
[UTchl-ll]
・Stage4
1995年以降の先行研究
・Stage5
数値的側面 ([IUTchlV],[ExpEst])

IUT批判者は、第三者が検証できる証明しか認めない数学至上主義者

IUT理解者は、従来の数学観にとらわれず、より相手を罵倒できた方が正しいという柔軟な思考の持ち主

とりあえずマトモな論文誌なら証明に重大なギャップが見つかったら撤回させるけど

だよナ

既存のLeanでは、HoTTのUnivalenceを定理として導入することはできない。通常は公理（axiom）として追加するしかない。そして、公理として追加した場合、その公理に対応する計算規則（computation rule）がないため、その部分はカーネルによる計算・簡約（reduction）ができない

これに反論できるleanの専門家いるの？
まぁHoTTを要するかは別問題だが、トートロジカルな部分の型計算って意味では、AIは真っ先にキュービカルAgdaを思いつくらしいね

HoTTであち～

speciesは何らかの数学上の「概念」で
mutationはある「概念」を別の「概念」に引き写す操作
みたいな？
なんか圏論（object/morphismとfunctor）と大して違いないような

>>388
みんな思ってるけど、言ったらブログで罵倒されるから言えないだけ

ブンゲンは昔から絶対にIUTが正しいとか一言も言ってない
新しい体系が必要とか素人向きの本書いたり
ZEN大学で企画ぶち上げたりLANAにかんだり
望月の親友ポジを強調するだけで真偽は自分にはわからないで
一貫してるよ

圏論ベースだからね
標準的な圏論との違いは複数の宇宙とその間の通信（Θ-link）を考えること

そして望月が思った以上にとてつもなくデカいlog-shell

ぶんげんってスネ夫だもんね完全に
チャンスがあればジャイアンの寝首も平気でかくw

ブンゲンは最悪トンズラできるように私はIUTを理解していないスタンスを取ってるからな

無駄に改行入れて的外れなLLMコピペ連発するIUT擁護派の精神分裂w

>>391
複数の圏とその間の関手でいいのでは

text【微分方程式 y' = -e^(-xy) (y(0) > 0) の有限時間発散の厳密な証明】

この方程式の解が、有限の x で「必ず -∞ に発散（爆発現象）する」ことの証明の大筋です。
論理は以下の2ステップで完結します。

1. 負の領域への進入（背理法）
すべての x >= 0 で y(x) >= 0（正のまま存在）と仮定します。
このとき積は常に xy >= 0 なので、指数関数の性質から e^(-xy) <= 1 です。
元の式に当てはめると、導関数の上界は常に y' <= -1 となります。
これを 0 から x まで積分すると、 y(x) <= y(0) - x が得られます。
右辺は直線的に減少するため、x > y(0) では y(x) < 0 となり、最初の仮定に矛盾します。
したがって、解は永遠に正のままではいられず、有限の x で必ず 0 を通過して負の領域に入ります。

2. 有限時間での発散（比較定理）
解が負になったある点を (x0, y0) [ただし x0 > 0, y0 < 0] とします。
x >= x0 かつ y <= y0 < 0 の領域では、双方の符号が負であることから、
-xy >= -x0 * y が成り立ちます。
これを元の式に適用すると、次の微分不等式が作れます。
y' = -e^(-xy) <= -e^(-x0 * y)

ここで、右辺を等号とした比較方程式「z' = -e^(-x0 * z)」を導入します。
比較定理より、元の解は常にこの比較解以下（y(x) <= z(x)）になります。
この比較方程式は変数分離形なので厳密に解くことができ、以下の解が得られます。
z(x) = (1 / x0) * ln[ e^(x0 * y0) - x0 * (x - x0) ]

対数関数 ln(X) は、中身が +0 に近づくとき -∞ に発散します。
上式のカッコの中身が 0 になるのは、以下の有限の x_max のときです。
x_max = x0 + (e^(x0 * y0) / x0)

元の解 y(x) は、この z(x) よりも常に小さいため、遅くともこの有限の値 x_max に達する前に必ず -∞ へと発散（爆発）することが数学的に厳密に証明されます。

誤爆 orz

AI 優秀すぎる

>>399
知的障害者にはそう見えるんだろうな
バカがLLM使っても無駄な実例

そもそも文脈もないゴミを掲示板に貼り付けてクソ漏らすところが既に精神分裂

ショルツも間違ってたんだよバーカって言いたいからここまでグダグダ引き伸ばしたのか

ショルツェは何も間違ってない。彼はIUT語で書かれたIUTを無理やり数学に翻訳したうえで証明に失敗してると言った。
一方LANAは形式化に失敗し、IUT語で書かれたIUTは数学ではないと言った。
どちらも本質的には同じこと。

つまり、望月は不当なsimplificationだと批判したが、そもそもIUTが数学になってないからsimplificationしたまでであって、問題の根本はIUTが数学でないことだ。
間違いなのではなく、そもそも正誤を判断する対象ですらない（Not even wrong）。

ホントその通り
それなのに問題点を指摘したS-Sを悪役にして
指摘を罵倒で返したMや論文を通したRIMSは無問題って
控えめに言っても（自粛）ですね
https://note.com/katobungen/n/nbf629d03ad80
＞Scholze-Stix報告は、その影響力の大きさから、IUTは単純に
＞間違っているという印象を強く世界に押印しましたが、
＞それは非常に不幸なことだったと思います。"

アティヤがリーマン予想証明した言うても向こうの人も半信半疑だったのに日本人だとなんでこうなっちゃうんだろうね

加藤和也の名前の字面がいつ見ても加法的整数論

世界で2番目のIUT理論研究拠点
IUGC (後に突然ZMCへ改称)を設立

⚫︎加藤文元所長.
IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。
⚫︎アナウス.
abc予想を解決したIUT理論。

1.
加藤文元発言とアナウスは
原因と結果の因果律も矛盾している
⚫︎
フェセンコ
・そもそも概念や使う言語など
従来の数学論文とIUT理論は
違うので完全に理解するには3年
かかった.

⚫︎梅崎
IUTTの単位を4つとも取るのは
かなり難しい

2
世界でIUTの理解者は20人程度
と言ってるが、
加藤文元.フェセンコ.梅崎は
IUTの自称理解者でしょ。
文元IUT本は望月新一監修だから
意義がある。
LANAは星(RIMS)以外がIUTど素人 のメンバーなのに、
星は今回もIUTへ質問から逃亡した。

3
k.kedlayaはk.joshiよりIUTど素人なのにk.joshiはメンバーから
はずれている。

4
IUGC(現在　ZMC)の加藤文元発言
>IUT理論と現行数学との違いを完全に言語化する新しい数学の言語体系を早急に作らねばならない。

は、当然、LANA中間報告の加藤文元発言が回答だろうね？

https://m.youtube.com/watch?v=8vLQIAgFapk&ra=m

IUTほど徹底してIUT語を前面に出して比較写像を無視した
「比較不能性」理論の中核原理に据えた数論は前例がありません。

>>405
忖度が美徳の国ですから

なんかXに3.12の解決策みたいなのを提示している人がいるな
アカウントがキリル文字の人

>>410
何で論文で出さんと？

ようやく国外でも報道があったよ
https://www.newscientist.com/article/2580313-effort-to-solve-biggest-controversy-in-mathematics-has-made-no-progress/
Effort to solve biggest controversy in mathematics has made no progress
『進展なし』だってさｗ
＞“Most people believe that there is a serious gap,”
＞“And I think that this particular report is fully consistent
＞with that: it has not managed to formalise it, which is what
＞we would expect if this big theory had some serious gaps.”

結局「人間に理解できる証明がないのに形式化なんて出来るわけない」
って前々から言われてた通りの結果になったよね

論文の行間が広すぎて理解できないってことならあるあるだけど
本当に証明があるんだったらすぐに詳細を補えるはずでしょ

それが出来ないのなら証明もないのにポエム読んで
理解した気になってただけってこと？

>>410
IUTの難しさは望月が思春期の女ぐらいの気持ちで禁止してることと許可してることを雰囲気で決めてるからで、最近のタオがやってる謎の解析のほうが完全に難しいだろ

とか言ってるしもう弄ってるだろコレ

>>412
加藤の安っちいポエムとかなw

>>413
>最近のタオがやってる謎の解析
とは？

尊師の声明もないし完全敗北だな

>>416
年始の謎日記で爆発w

>>412
そう。IUTは望月新一語で書かれたポエム。
LANAが示したのはポエムは形式化できないという当然の結果に過ぎない。

>>416
SSのときと違って今回は身内の星だから何も言えんやろね

IUTについて興味がある人にSSはなんで間違っていたかを説明するとactual q-pilot images/anabelian reconstructionはpoly-isomで結ばれ、compatibilityによりlog-volume集合は一点集合になるのだが、SSは異なる経路からの二点が一致せずに矛盾すると言っている。つまりより最悪なことが起きている

IUTの国ではICMは開けないってよ
はやく撤回してね