Interuniversal geometry とABC 予想61 


ほんまやね。まぁそのうち証明されるやろけど。たぶん純理論的には問題ない。一部残ってるかもしれないヒューマンエラーが洗い出されれば安心して使えるでしょ。Lean の基礎理論(数学部分)とコーディング部分の正当性を Lean に検証させるプロジェクトも実行中らしいし。それが通ったらもう信頼性はほぼ完ぺきになるやろな。

最近は話題にならなくなった

>>926
7/17に中間発表だから年明けに最終発表がある
スケジュール考えると数学的結論は10月末頃には出てないといけないだろう
中間発表で結論は出てるから望月の同意を得られるかどうかしか争点はないが

そもLeanに翻訳するのが難しいと言われるといつ終われるのか分からんな


【ReHacQ生配信】AIで数学を証明!?IUT理論は正しいのか【高橋弘樹vs川上量生vs野村泰紀vs加藤文元】
https://www.youtube.com/live/b6JlM_nrM3M


━━ LANAプロジェクト（IUT理論の検証プロジェクト）の進捗状況については、1時間03分30秒頃から語られています。加藤先生と川上氏が、プロジェクトの中間発表の内容や、現在の到達点について詳しく説明しています。

•判断の保留: 現時点では理論が正しいか間違っているかを断定する段階には至っておらず、引き続き検証が必要な状態であること（1:03:32-1:04:10）。
•言語化の壁: コンピュータ言語（Lean）へ翻訳するための前提となる人間側の理解において、まだ解明すべき難所があること（1:04:11-1:07:25）。


━━ 遠アーベル幾何学の内容をコンピュータ言語である Lean に落とし込むプロジェクトについての話は、1時間36分49秒頃から始まります。

このパートでは、IUT理論の根幹をなす遠アーベル幾何学を計算機上で扱うことの難しさと、なぜそれが重要なのかについて以下の点が語られています：

• IUT理論と計算機科学の接点: IUT理論自体は非常に難解でキャッチーな話題ですが、その土台となる遠アーベル幾何学を Lean に落とし込むこと自体が、数学研究における新しい手法として重要であると説明されています (1:36:51-1:37:04)。
• プロジェクトの意義: IUT理論を検証する過程で、この基盤となる理論をコード化することは、現代数学の新しい検証手法としての大きな実績になるという議論がなされています (1:37:05-1:37:14)。

今までは権威で逃げ続けてきたけど
AIとLeanがたいていの数学者より信頼できるようになった今はもう通用しないだろうな
尊師は定年までゴネ続けるんだろうけど
付いていった任期付きの取り巻きたちの敗残軍は残りの人生どうすんのかなw

>>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とか興味ない