Interuniversal geometry とABC 予想61  

Interuniversal geometry とABC 予想61   (430ﾚｽ)
上下前次 1-新

264(4): 07/19(日)17:56 ID:/DrSmv+b(2/2) AAS
LANAが形式化に失敗した理由は、はっきり言って、
理解者以外の人がやってるからじゃねーか？
だってIUTグループ内ではLean code（非公開）が
すごく役立ってるらしいっすよ
外部ﾘﾝｸ:aitpm.github.io
>The skeletal Lean code that we wrote for this portion of IUT
>constituted a remarkably successful case of the use of Lean
>as a communication tool.

あれだよ、あれ
零と交信できるとか透視できるとか主張する人によくあるやつ
省6

265: 07/19(日)17:59 ID:dIige2Ai(1/12) AAS
>>260
>今後ギャップが埋められるかどうかはまた別の話としても

埋められるわけねえ
出来るもんなら8年前にショルツがやってる
あるいは京都で会って議論した時に望月が

266(1): 07/19(日)18:03 ID:cgLsEX0O(7/7) AAS
みんなアホレス過ぎて返事する気にもならん

267: 07/19(日)18:03 ID:dIige2Ai(2/12) AAS
>>264
気の所為です
だって8年前のss論文の指摘通りだったんだから
コミュニケーションツールとして役立って数学的な理解が深まったわけじゃない

数学的直感だけに頼った間違いを追求する拷問道具として役立っただけだ
間違いを論理的に詰められることは数学者にとって拷問なんですよ

268: 07/19(日)18:04 ID:dIige2Ai(3/12) AAS
望月は京都で議論した時に気付いてたはず

269: 07/19(日)18:20 ID:S1PMNEss(6/9) AAS
gtrのおっさん
何度論破されても理解できないw

270: 07/19(日)18:22 ID:S1PMNEss(7/9) AAS
論破されていつものこれw
redditがあ愚か者でえええ(根拠ゼロの遠吠え
言語力ゼロ論理力ゼロw
IUT仕草そのもの
👇

266 １３２人目の素数さん sage 2026/07/19(日) 18:03:13.41 ID:cgLsEX0O
みんなアホレス過ぎて返事する気にもならん
2chｽﾚ:math

271: 07/19(日)18:45 ID:dIige2Ai(4/12) AAS
redditの論調は変わってないけどな
IUT理論はもう終わってるし
望月は現在の数学者コミュニティでは認め難い人格破綻者という事で
この発表前からそうだった
数学者コミュニティは対話拒否には耐性があるが
他研究者への人格攻撃には慣れてなかった
ペレルマンが中国人研究者に怒ったことはあったけどな
最終的にポアンカレ予想を解いたのは我々という主張に

272: 07/19(日)18:57 ID:tZJSVLSb(1/9) AAS
>>247
>その証明の部分を今後追加していける可能性があるんだよね？
すべての未解決問題がそうだけど？

>望月新一憎しの怨磋だけで叩いてこき下ろしてるとしか思えん
ショルツェ憎しの怨磋だけで叩いてこき下ろしてるのが望月な

273: 07/19(日)18:58 ID:sLQxBWTV(1) AAS
IUTが正しいかどうか知ったこっちゃないが、
カトブン妄信とか恥ずかしすぎだろwwww

274(1): 07/19(日)19:02 ID:tZJSVLSb(2/9) AAS
>>249
>PRIMSは証明なしでABC予想を解決したとする論文を受理したが、まだギャップがあると断定してないので撤回する必要もない
>RIMSの形式化作業を待つしかない
IUT理解者の星参加で形式化できなかったんだから望月論文はギャップありで確定やろ
今後の可能性は別の話だ

275(2): 07/19(日)19:06 ID:dIige2Ai(5/12) AAS
>>274
加藤も望月と対話してるよ
武士の情けで何を話したかは書いてないだけで

276(2): 07/19(日)19:12 ID:dIige2Ai(6/12) AAS
ZEN大学LANAプロジェクトの公式見解は中間報告書通りだが
加藤個人の見解はこうだよ

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

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

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

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

278: 07/19(日)19:19 ID:tZJSVLSb(3/9) AAS
>>254
解かない可能性もある
数学で可能性をあーだこーだ言ってもしかたない
ってみんな言ってるんだけど、君、馬鹿？

279(1): 07/19(日)19:26 ID:dIige2Ai(8/12) AAS
>>275
加藤望月対話の根拠ね
加藤は対話という表現を一貫して使っているが
内容はギャップについての数学的な議論のはず

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

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

(以下略

280(1): 07/19(日)19:27 ID:tZJSVLSb(4/9) AAS
>>258
>まだアウトじゃない
加藤本人が解決には無限時間かかる（＝解決できない）かもしれないって言ってるんだから何の意味も無いんだよ

281: 07/19(日)19:28 ID:dIige2Ai(9/12) AAS
>>276
この等式の呟きもIUT理論によるabc予想でのミスの話だったわけだね
中間報告書を斜め読みする限りでは

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

282: 07/19(日)19:30 ID:tZJSVLSb(5/9) AAS
>>260
その通り。
今後の話は別の話。だって今後どうなるかは誰にも何も分かってないんだから。

283(1): 07/19(日)19:36 ID:tZJSVLSb(6/9) AAS
>>264
星氏は理解者じゃないと？

284: 07/19(日)19:41 ID:tZJSVLSb(7/9) AAS
>>264
>すごく役立ってるらしいっすよ
コミュニケーションツールとしてな　検証ツールとしてとは書かれてない

285: 07/19(日)19:42 ID:tZJSVLSb(8/9) AAS
>>266
じゃ返事しなきゃよい

286: 07/19(日)19:44 ID:S1PMNEss(8/9) AAS
>>283
都合悪いから星を切り捨てたんじゃねw
IUT仕草ってやつww

287: 07/19(日)19:45 ID:S1PMNEss(9/9) AAS
>>264
gtrおじさんのダブスタ出ましたーー

288(1): 07/19(日)19:52 ID:tZJSVLSb(9/9) AAS
>>275
対話で埋まるギャップならとっくに埋まってるやろ　望月は証明が正しいことを完全に理解してるはずなんだから
埋めるための対話じゃないのは明白

289: 07/19(日)20:08 ID:dIige2Ai(10/12) AAS
>>288
実際は加藤によるギャップがある事の説明と
望月による数学的釈明のはずだけど
まあ武士に情けではっきりとは書いてないわな
>>279で議論の目的ははっきり分かるけど

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

290: 07/19(日)20:33 ID:vLR4xaTQ(1/3) AAS
>>280
はっ！
これは
史上初の
「無限の長さを持つ証明」
ではないのか？
ヒルベルトもゲーデルも間違っていた！？

291: 07/19(日)20:56 ID:LV6JyMJX(3/4) AAS
この点に関する望月氏の追加説明が今も続いているため、現時点では最終的な判断を留保しています。

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

292: 07/19(日)21:02 ID:vLR4xaTQ(2/3) AAS
パネルディスカッションにしてくれないかなあ
望月さんとleanチームやショルツスティクスとの対話
すぐには終わらないから無理か
でも延々やって貰っても良いんだけどね

293: 07/19(日)21:07 ID:LV6JyMJX(4/4) AAS
望月が絶対に表に出ないから退職してからよ

294(1): 07/19(日)21:10 ID:Rq7nehTH(1/3) AAS
一般に証明ができたという主張を批判する場合には、間違っていることを証明する必要はなくて、容易に埋まらないギャップの存在を指摘すれば十分です。

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

295(1): 07/19(日)21:13 ID:vLR4xaTQ(3/3) AAS
「埋められる・・・
埋められるが・・・
いつ埋められるとは言っていない」
みたいな？

296: 07/19(日)21:15 ID:dIige2Ai(11/12) AAS
>>294
この報告と大筋で変わりないって書いてあるしね

297(1): 07/19(日)21:15 ID:dIige2Ai(12/12) AAS
>>295
カイジ乙

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

299: 07/19(日)21:24 ID:Rq7nehTH(3/3) AAS
はい！モッチーの証明は失敗でした！

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

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

300: 07/19(日)21:44 ID:cp7Tg8RZ(2/2) AAS
よし、とりあえず論文撤回しようね

301: 07/19(日)21:59 ID:PUqsP0tr(1) AAS
なんかツイッターから批判的な論説をコピペして悦に入っている人がいるな

302: 07/19(日)22:01 ID:/UFaYt6V(1) AAS
>>297
反論出来ないIUT擁護派おじさんの哀れなゴミレスで爆笑w
お前どこ卒だよマジでw

303(1): 07/20(月)01:42 ID:FZIBLfcu(1) AAS
>>245
woitのblogならそもそもwoitと仲良いやつや捨てアド以外のまともな学術機関のメールアドレス開示するやつのコメしか承認されないだけだぞ
むかーし捨てアドだけど使えるメアドでふっつーのこと書いても承認されなかったしな

304(1): 07/20(月)01:44 ID:AtZID/Oc(1/10) AAS
>>303
被害妄想くっそわらたw

305: 07/20(月)01:45 ID:AtZID/Oc(2/10) AAS
じゃあredditはw

306(2): 07/20(月)01:56 ID:joumQYeu(1/8) AAS
redditにもトピック立ったんだ
前見た時ないからみんな興味ないのかと思ってたわ
あと日本人は英語苦手だからじゃない？
見てみよ

307(1): 07/20(月)01:59 ID:B6WVrHSM(1/7) AAS
>>306
URLは？

308: 07/20(月)02:15 ID:joumQYeu(2/8) AAS
>>304
被害妄想なのか果たして、昨日またコメントしたけどダミーメアド使ったから公開されんかもね

309(1): 07/20(月)02:16 ID:joumQYeu(3/8) AAS
>>307
r/mathにあるよURLくらい自分で探そ

310: 07/20(月)02:19 ID:B6WVrHSM(2/7) AAS
>>309
出せないんですね
これじゃね？
外部ﾘﾝｸ:www.reddit.com

311: 07/20(月)02:26 ID:uYiIkRIQ(1/4) AAS
>>306
継続的に話題にはなってるよ
つまんないからすぐ終わるだけで

312(4): 07/20(月)02:34 ID:joumQYeu(4/8) AAS
てかr/mathもコメント承認制か？コメントしたけど自分以外からは見えないわ
ブラウザ変えたら見えなくなった
そら擁護派のコメントとか見えんわけだわ

313(1): 07/20(月)05:31 ID:PSm97/0a(1/2) AAS
ブンゲンさんって日本語と英語で言ってることが微妙に違うよね
↓の英語では論文中に形式化可能な証明の記述がないことを
明言してるけど、日本語では「現状では不可能です」って
誰の責任か分からない曖昧な物言いになってる

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

外部ﾘﾝｸ:x.com
＞Fumiharu Kato 加藤文元（Bungen）
＞@FumiharuKato 4:19 PM · Jul 17, 2026
＞本日の記者会見のまとめです：
省18

314(1): 07/20(月)05:46 ID:PSm97/0a(2/2) AAS
ブンゲンさん、LANA記者会見では、
S-Sの指摘とLANAの指摘したポイントは基本的に同じ、
しかし自分たちはより解像度が高い
って言ってるし（1:01:00〜ほか）、
S-Sを批難することは避けてるけど、
日本語の「仮想的質疑応答」では
外部ﾘﾝｸ:note.com
＞結論から申しますと、我々の報告とPeter Scholze氏および
＞Jakob Stix氏の報告の内容は本質的に異なっています。
＞そして、我々は彼らの誤謬を指摘することができます。
省1

315: 07/20(月)06:18 ID:B6WVrHSM(3/7) AAS
redditって自動翻訳機能あったよな

316(2): 07/20(月)06:42 ID:B6WVrHSM(4/7) AAS
>>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.

外部ﾘﾝｸ:github.com

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

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

318(1): 07/20(月)07:10 ID:joumQYeu(5/8) AAS
>>316
それだよ
やっと承認されたか
woitの方にも似たこと書いたけど承認されんわ

319: 07/20(月)07:46 ID:uYiIkRIQ(2/4) AAS
>>313 >>314
英語の方が本音です

320: 07/20(月)07:47 ID:uYiIkRIQ(3/4) AAS
>>318
多分本人がやってるから時間かかってるだけじゃんないかな

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

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

322(1): 07/20(月)07:58 ID:uYiIkRIQ(4/4) AAS
ホモトピー型理論は既にLeanにもライブラリがある

323: 07/20(月)08:16 ID:B6WVrHSM(5/7) AAS
>>312
>そら擁護派のコメントとか見えんわけだわ
擁護派そのものじゃないかもしれないが
ショルツスティクスさんの間違いを指摘できるというコメントは読めるけどね

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

325: 07/20(月)08:23 ID:nz34QvDF(1/4) AAS
十数年正しいって思い込み続けてたものが
無意味で荒唐無稽なゴミだったって自覚したら自殺するのかな尊師は

326(1): 07/20(月)08:47 ID:JYTnQtYq(1) AAS
自覚あるけど沈黙して終わり
数十年後の数学史にどう名が残るか
ブンゲンもそうだけどね

327(2): 07/20(月)09:22 ID:39P46wHw(1) AAS
指摘を受けた時点で問題点は認識していたと思う。でも、IUTを前提にキャリアを積んできた弟子達のために、撤回という選択肢を取れなかったのでは。

328(1): 07/20(月)09:27 ID:tXBgWMjQ(1) AAS
ずば抜けた存在と一旦認められてしまえば
そのあとでごみ論文を書いたとしても
名は残る

329: 07/20(月)09:41 ID:fLoZ2FvT(1) AAS
>>321
>俺の独自物理理論

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

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

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

331: 07/20(月)12:32 ID:AtZID/Oc(3/10) AAS
いつも通り、IUT理論が間違っていると結論づけた愚か者たちは事実関係を歪めるのに忙しい😂🤣 reddit.com/r/math/comment…

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

332: 07/20(月)12:35 ID:AtZID/Oc(4/10) AAS
>>312
どういう書き込みしようとしたのか見てやるよ
どーせここと同じで文にすらなってない気狂いのお前がクソ漏らしてんだろww

333: 07/20(月)12:36 ID:AtZID/Oc(5/10) AAS
プーアノンっぽいアイコンで爆笑w

334: 07/20(月)12:45 ID:AtZID/Oc(6/10) AAS
>>316
LLM英語丸出し
そしてすでに証明したとかいうキチガイ言及はできず

ビビリキチガイw

335: 07/20(月)13:01 ID:AtZID/Oc(7/10) AAS
>>321
数学に向いてないんよ
数学になってないゴミだから

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

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

337: 07/20(月)14:35 ID:9bql5oHW(1/2) AAS
>>327
お優しいですね

338: 07/20(月)14:36 ID:9bql5oHW(2/2) AAS
>>328
アチャ～

339(1): 07/20(月)15:46 ID:nz34QvDF(2/4) AAS
望月怪文書も出ないしもう白旗あげたんだな
文元にも梯子外されてブルータス、お前もか状態w

340: 07/20(月)15:50 ID:nz34QvDF(3/4) AAS
アホのmathjinがまたご都合解釈でショルツスティックスを悪者にしてキャーキャー騒いでるけど現実はこう

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

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

341: 07/20(月)15:52 ID:R14n4V8q(1) AAS
>>326
少なくとも日本の数学史の汚点としては確実に残る。

342: 07/20(月)15:55 ID:nz34QvDF(4/4) AAS
まあ一族郎党末代までの恥だよな
あれだけ自明自明ってゴネ続けて批判者にハラスメントしまくってたのに
その結論が8年前のSSレポートの通りでした！だもんなぁw

343: 07/20(月)16:18 ID:raUhjEv+(1) AAS
>>339
関連スレにいるキチガイAIおじさんとmathjinしか味方がいないw

344: 07/20(月)18:19 ID:AtZID/Oc(8/10) AAS
IUT擁護派おじさんが発狂コピペしててワラタw

【数学】「ＡＢＣ予想」巡る望月新一教授の証明、検証チーム「不明瞭な点がある」と中間報告 [すらいむ★]
2chｽﾚ:scienceplus

345: 07/20(月)18:41 ID:6IFkcsnz(1) AAS
ショルツェに後れをとってしまったようだね？

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

347(2): 07/20(月)20:11 ID:4622Ml0Y(2/2) AAS
>>324
何いってんだか
君はまさか新しいロジックだとでも思ってるわけなのか

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

349: 07/20(月)20:57 ID:joumQYeu(8/8) AAS
>>347
新しいロジック？？どう言う意味？

350: 07/20(月)21:26 ID:nvAAFNKw(1) AAS
ブログで法の支配とか適正手続を強調してたんだから一応適正手続が保障されて納得はしてるんちゃうの

351: 07/20(月)22:23 ID:AtZID/Oc(10/10) AAS
IUT擁護派おじさんついにバックレるの巻

👇

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

ってか、査読システムが全く機能してねーのに、査読論文数とか被引用数で研究業績評価するから、世の中は屑論文であふれてるわけな
2chｽﾚ:scienceplus

352: 07/20(月)22:36 ID:B6WVrHSM(6/7) AAS
理解してないのに何か擁護できると思っているのは不可思議ですね

353: 07/20(月)22:38 ID:afIwWzT/(1) AAS
そりゃそう思うわな LEAN でできることできないことが全くわかってないんやろ
LEAN で形式化できないならもうそんなもん数学の論文でもなんでもないというのがわかってない
そのレベルのあんぽんたんなのにわけもわからずでかい口たたいてんだからたたかれて当然やわな

354: 07/20(月)22:39 ID:IyeyWlPF(1/2) AAS
問．次の三者の意見から仲間外れを探しなさい

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 ＠動画ﾘﾝｸ[YouTube]　50:00〜
省4

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

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

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

356(2): 07/20(月)23:02 ID:GA8zqCsb(1) AAS
MathlibにZFC形式化を実装させればspecies/mutationの形式化はできるんじゃないの？
それができれば、解決に近づく

357: 07/20(月)23:31 ID:B6WVrHSM(7/7) AAS
>>356
>species/mutation
て何？

358: 07/21(火)01:27 ID:9lPB4r8c(1/4) AAS
IUTが形式化できなければ
>そんな等式は"tautological"な理由により成り立つ
は数学の主張ではなくただのお気持ち表明。
さあ困ったね望月さん。

359: 07/21(火)01:58 ID:0mZfL8hO(1) AAS
RIMSもIUTの形式化に取り組んでるらしいね
LANAが形式化に失敗してRIMSが形式化に成功したと言って対立したら面白い

360: 07/21(火)02:15 ID:Jsxsb6pu(1) AAS
>>356
ZFCのライブラリはあるし
中間報告書もそんな事は問題にしてない

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

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

363: 07/21(火)03:40 ID:g8yakgFo(1/2) AAS
致命的なギャップを聞く耳持たずで自明自明言い張り続け
指摘者に圧力かけまくり誹謗中傷しまくりだった恥ずかしい老害、leanでトドメを刺されて死亡

上下前次 1-新書関写板覧索設栞歴

あと 67 ﾚｽあります
ｽﾚ情報赤ﾚｽ抽出画像ﾚｽ抽出歴の未読ｽﾚ AAｻﾑﾈｲﾙ

ぬこの手ぬこTOP 0.038s