Interuniversal geometry とABC 予想61 



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

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

>>929
笹川朝鮮財団に媚びて生きていくしかないんじゃねーのか
惨めだわな

>>925

>まぁそのうち証明されるやろけど。たぶん純理論的には問題ない

健全性が証明されていないなら
数学の証明として不完全でしょ。
L ANAはzen大学の話題ほしさと
scholzeたたきの茶番劇ですね。
leanのコンパイラカーネルを無理やり通過したからOKなんだろうなあ、

「LEANが証明したLEANの正しさ」ということを真面目に信じてよいものであるかどうか。
あるところに嘘つきがいて「私は正直者ですよ」というのとあまりかわらないことになるのでは？

FLTのleanによる定理証明支援系
では元々確立した自然言語の
Wiles–Taylorの証明がある。

一方、
望月新一独特のIUT語による
「 abcの証明」はzen大学を含むとりまきと日本しか通用していない。実際
IUTはICM2026のlectures
にもなかった。

Leanが通らなかった以上どれだけショルツの揚げ足取りしようが望月サイドの完全敗北だろ

あほなんじゃないのかな？健全性に疑義がのこるってのは「正しくないのに正しいって判定される可能性がある」って意味なんだけど？あほなん？

Lean以前に証明を誰も追えないのが望月さんの証明
形式化以前に誰も納得してない
正しいと言ってるほんのごく少数の人間も他人に説明出来ない
星さんの苦渋のコメントを読んでみろ
納得出来てないだろw
Lean関係ない
全く関係ない

>>928
>• プロジェクトの意義: IUT理論を検証する過程で、この基盤となる理論をコード化することは、現代数学の新しい検証手法としての大きな実績になるという議論がなされています (1:37:05-1:37:14)。

研究者のキャリア上重要な業績になるようなことじゃない
他の事やるよ
まあ望月の証明が正しければ話は少し違うんだが

もしもIUTを仮定すればRHが導けたら面白いだろうね。

iutを仮定したらなんでも解けるんじゃね？

・(>920) (>921)-(>>924)

『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

・
Postmortem for Kernel Soundness Bug #14576

> Verification
Mario Carneiro's lean4lean is a Lean formalization of Lean's type theory together with a proof that the kernel implements it.
The work is ongoing, the proof of consistency does not cover inductive types yet, and the
to-be-verified implementation suffered from the same bug as the official kernel.
The bug would have been found when attempting to conclude the verification of this part.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

まだいってるよ。lean 3 から lean 4 への拡張って let rec の追加、structure η と浮動小数点計算のなんからしい。そして lean 4 があぶないならたとえそれでOKでも Lean 3 では通らない可能性があるにはある。しかしその場合 let rec を全部はがして top level 再起に書き換えて structure ηの証明を書き加えたらそのまま lean 3 で通せる。そして lean 4 でダメなやつは lean 3 でもダメ

てかそもそも lean 4 がまだ信頼でいないなら lean 3 でかけばいいやろ

>>942
leanのせいにしたいんだろ

正直もうabcとか興味ない