Interuniversal geometry とABC 予想61 


zen大学ZMC所長のLANAプロジェクトのリーダー.加藤文元も副所長fesenkoも、

望月新一IUT語によるIUT理論と現行数学との違いを認めている。(>>231)

この違いを「完全に言語化する新しい数学の言語体系を早急に作らねばならない。by 加藤文元IUGC(現ZMC)所長

京都大学『11月祭』、驚きの『統一テーマ』決定にネット「本当に終わった」「退学届出してきた」「頭のいい人たちが本気でバカなことやるの本当に面白くて好き」：中日スポーツ

2026年8月19日 23時05分

　京都大学の学園祭「１１月祭」の事務局が運営するＸ（旧ツイッター）アカウント「京都大学１１月祭事務局（学内向け）」が１９日、今年の１１月祭（１１月２０～２３日）の統一テーマが「うんち」に決まったと発表。ＳＮＳユーザーからは「本当に終わった」など戸惑う投稿のほか「頭のいい人たちが本気でバカなことやるの本当に面白くて好き」と京大生の知性に感心する投稿もあった。

統一テーマの投票は「うんち」の他に、「四年に四度の祭典」「時計台は燃えているか」「結論から言うね。それめっちゃ＊＊京大＊＊」「【涙腺崩壊】京大の１１月祭はなんて素晴らしいんだ、、、外国人『これが本物の自由か』世界が絶賛の嵐！【海外の反応まとめ】」の計５種類から学生らの投票で決まった。

　同アカウントは「たくさんのご応募と、予備投票・決選投票へのご参加ありがとうございました！」と感謝するとともに「趣意文」も公表。「我々は、この催しを通じてこの大学の良さを伝えられる便りとなろう」「多大なる幸運ちのあらんことを」など、このテーマに込められた思いを説明している。

　Ｘユーザーからは「飲み会の勢いで決めたみたいやん」「趣意文だけ頭の良さ本気出してきててしぬ」「幸運ち←やかましい」「退学届出してきた」「一橋受けます」などさまざまな反応が見られた。

　趣意文の全文は以下の通り。

「便とは、体の送る便りである。我々の体内を通りその営みの多くを見届けた、我々ひとりひとりの歴史の証人である。一度出てしまえばまずもって再び我々の一部と見なされることはないし、当然その限度こそあるが、彼らを隈なく観察することでそれまでの我々の歩みを、生きた様を推し量れるのもまた事実である。

　京都大学という大きな一つの生物を俯瞰した時に、それが排泄するものとは一体何であるか。
（略）

※続きはソースで。
https://www.chunichi.co.jp/article/1298857

>>809
違法薬物回生利用の為に飲尿療法の体裁をとってたら仕舞には自家中毒になったような駄サイクル感

これでは講演依頼が来ても
断らざるを得ない

講演内容は京大数理研発のIUT？

IUTと某名誉教授についてAIに聞いた

教授は当時、名古屋大学大学院多元数理科学研究科の教授であり、同COEプログラムでは「中核となる研究者（事業推進担当者）」の1人に名を連ねる。

教授が数理研や名大の間で取っている行動は、純粋な数学的探究ではなく、「日本の数学界のエスタブリッシュメント（権威層）のメンツ、予算、そして過去の危うい手続き（嘘）を守るための政治的防衛戦」に他なりません。
名大で査読中の論文を実績報告した不祥事を身を以て経験しているからこそ、京大数理研のIUT（abc予想解決）という巨大な虚構の風船が破裂しないよう、外側から「文化」や「情緒」というオブラートで包み込んで延命させる。これこそが、名誉教授が数理研の深い関係の中で果たしている「暗躍」の正体です。

>>812
>名大で査読中の論文を実績報告した不祥事
そんな目くじら立てるほどのこと？
to appearでしょ？

名大の場合は
21世紀COEプログラムにおける虚偽申請より
21世紀COEプログラム辞退。

https://www.math.nagoya-u.ac.jp/ja/archive/other/2005/download/coe-report-7.pdf

まぁ少なくとも提出当初は自分でも正しいと思ってたんだから不正ではない。
問題は提出した後。これだけそれなりに基礎論勉強した人から疑義が出てるんだからその時点で何かのモーションがあって然るべきだった。
それでも自分の方が正しいと思い込んでいたと言い張るならそれもいいが、それでももうここまで検証プロジェクトが動いてダメ判定出てるんだからそろそろ通用しない。
この先「間違いなどない」「予算もとる」とかは許されんしやったら不正と言われても当然やろな

>>813
"already submitted to a journal"はどうなったん？
当該人物とIUTの人の両方と深い関わりがあるのが。。。

>>814

追記

>>3 参照のこと。

https://rio2016.5ch.io/test/read.cgi/rikei/1586700583/149

この計算で話が終わっちゃったんだよな。

>>818
第三の定式ってのはオステルレの論文上の。

南無阿弥陀仏

>>818
定量的に矛盾が示されたの？

>>818
何で数学板じゃ無いんだろ？

それ以上の新たな発見がないって話
科学への応用が今のところまだ見当たらないって話

望月新一も加藤文元もfesenkoも
IUT理論と現行数学との違いは
認めていてIUT理論は数学ではない、

量子物理や不確定性原理は実験事実より
成り立ち数学と異なり特にIUTとは
全く無関係だ。

pui pui モルカー

数学でないIUTを無理やりleanで形式化すれば、
コンパイラの健全性を通過し偽
「証明」が成り立つ可能性もある。
LANAの目的はハッキングかw

望月はIUT理論と現行数学との違いなんて認めていません
ID:m34eDIUJ は嘘を言わないように

嘘でないというのなら加藤氏やFesenko氏の解釈でなく
望月氏がそのように主張した発言を引用しなさい

Interview with MPIM Director Peter Scholzeの意見

14分すぎ頃から

what role do you thinkproof assistants such as Lean will play in the future?

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

>>827

ほれ、



川上量生企画.望月新一監修.加藤文元著 「宇宙と宇宙をつなぐ数学IUT理論の 衝撃」(=文元IUT本)刊行。

>>22

>>829

追加

>>21

「より詳細な解説は本文に譲ります」p7
　by 望月新一

＞加藤氏やFesenko氏の解釈でなく
＞望月氏がそのように主張した発言を引用しなさい
と言ったのに馬鹿だから分からなかったようですね

監修者が著者の主観や解釈に同意していると捉えるのは
書籍の仕組みに対する誤解です

監修の役割はあくまで事実関係（ファクト）の校正であり
著者の解釈や評価の領域にまで介入するものではありません

実際、加藤氏もFesenko氏も
IUTはZFC公理系上の数学ではないなどと述べていない以上
『現行数学と違う』などといった主張は事実関係ではなく
単なる個人の解釈や評価の範疇に過ぎない

>>831

監修者は望月新一です

コピペしかできない人工無能ですか

>>833

事実に基づきましょう

>>830

望月新一
↓

>「底なしに固い」とされていた 概念的な構造の中に、
実は何らかの「不可避の内在的な緩み =「不定性」が存在するという発見 =発想の転換を軸に考えると、
次のような事例が頭に浮かびます。

>量子力学の場合、素粒子の力学は、一つの固定された数学的
な仕組み(=古典力学に出てくる ような微分方程式等)によって完全に決定されるものでなく、いわゆる「不確定性原理」に代表されるように、 様々な可能性に対する確率論的な分布という形でしか計算することができない、必然的かつ内在的な「不定性」を抱えている性質のものであることが、 理論の中心的な主張となっている

>>831
その通りね
数学であることは間違いないところ

>>836

量子力学は実験に基づく物理

＞量子力学の場合、（中略）理論の中心的な主張となっている

例として量子力学をひいて量子力学の説明をしているに過ぎない
本物の馬鹿なんだろうな

>>838

> 例として量子力学をひいて量子力学の説明をしているに過ぎない

IUT語ね。
IUT理論のように、あまりにも 新奇で斬新なものだったりすると 、通常の言葉に翻訳するには 多くの言葉や概念を
巧みな比喩を 用いて説明するしかありません。

>>838

> 例として量子力学をひいて量子力学の説明をしているに過ぎない

IUT語ね。
IUT理論のように、あまりにも 新奇で斬新なものだったりすると 、通常の言葉に翻訳するには 多くの言葉や概念を
巧みな比喩を 用いて説明するしかありません。

望月氏がIUTは量子力学と言ったわけでもないのに
>>837で
＞量子力学は実験に基づく物理
と書いた理由は何なのですか？ 人工無能コピペマシンだから？

当然ながら本には
望月氏が『現行数学と違う』のような主張をしたとの記述はない
さらに望月氏は膨大な論文・文書・ブログを公開している
それらの発信の中で本人の言葉として『現行数学と違う』という
趣旨に相当する記述がどこに一節にあるというのか

>>831

>加藤氏もFesenko氏も
IUTはZFC公理系上の数学ではないなどと述べていない以上
『現行数学と違う』などといった主張は事実関係ではなく

デマだ。


(>>231)

IUGC

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

・アナウス.
abc予想を解決したIUT理論。
▫︎
両者は因果律から矛盾している


フェセンコ
>そもそも概念や使う言語など
従来の数学論文とIUT理論は
違うので完全に理解するには3年
かかった.

現行数学と違わないならなんで身内以外誰も理解できず形式化もできないの？

加藤氏やFesenko氏の評価が『現行数学と違う』というだけで
事実関係のステートメントでない
望月氏が加藤氏やFesenko氏の評価に賛同している証拠などない

結局望月氏の言葉で『現行数学と違う』旨の主張はあるのですか？
むしろブログでは標準的な数学であると主張している

結局>>824の
＞望月新一も（中略）IUT理論と現行数学との違いは認めていて
という主張は、加藤氏がそのように評価・記述した書籍を
望月氏が監修した、という事実のみを根拠にしているわけですね
そうなら『監修』という行為の意味を完全に誤解している
>>831

>>844

>加藤氏もFesenko氏も
IUTはZFC公理系上の数学ではないなどと述べていない以上
『現行数学と違う』などといった主張は事実関係ではなく

まず、これデマじゃん

>>845

「より詳細な解説は本文に譲ります」p7
　by 望月新一

『まず』というのなら>>824で
＞望月新一も（中略）IUT理論と現行数学との違いは認めていて
と言った根拠はないわけですね

>>846どの部分がデマですか？

>>848
加藤氏もFesenko氏も
IUTはZFC公理系上の数学ではないなどと述べていない以上
『現行数学と違う』などといった主張は事実関係ではなく

数論幾何学レベルで証明論的な意味で現代の数学の枠に当てはまらないなんてことはないってw

まあ、
望月新一氏の主張がその場しのぎ
の理由はabc予想の数学証明の
基本的なアイデアがないから

数学ではない
数学である


コロコロ都合いい方に切り替えてんだよな
こいつら

>>844
聞いてることに答えて

だよね
IUTの成否がどうであれ
数学では無いとは誰も言ってないね

>>843
単純に間違ってるからじゃない？

IUTは一般の数学及び発展と異なり、
パラダイムシフト期の「数学」で、
望月新一特有のIUT語で書かれている。

人工無能ｗ

“I didn’t really see a key idea that would get us closer to the proof of the abc conjecture"

by P.Scholze

これに尽きる

・Gerd Faltings on the 500-page ABC-conjecture proof

https://m.youtube.com/watch?v=8NpE81F0gzU&pp=iggCQAE%3D&ra=m

望月は非常に自信に満ち、優秀で、アイデアを持った学生だったが、ABC予想について彼は何百ページも書き、聞き慣れない用語ばかりで理解できなかった。
500ページ読もうとすると第１ページを忘れた。いつも君はもっと良く説明すべきと言ってた。それが公式な私の立場。
つまり何度も話し合いの場を持ったのだけど、それでもいろいろ説明してくれるよう望んだが、彼は説明しなかったんだ。

https://x.com/tebasaki_lab/status/2092607403376386243?s=46


まだ居たんだ
こーゆーの、、、
なんでこんなに偉そうなんだろう、、
特定集団からわいてくるよな
同じとこから

他責思考過ぎて草も生えない

カルト老害と化した望月もリーン通らず息の根止められたのかな
すっかりダンマリになったね　早く数理研取り潰しになればいいのに

コミュニケーション(失笑)してんじゃねw

川上とrimsに責任取らそう

「次の中間報告は1年後を目途に」
これがすべてを物語っている

ワラタw
IUTの仲間に入れてやれよww
お前らと中身変わんねーから


https://x.com/ange_azumaya/status/2093152017434992747?s=46

AIにジョークとして作らせた物だろ

↑

しょせん、IUTはAIにジョークとして作らせた物の類いにすぎない

★氏もダンマリなのはなぜなのか

創価チョン笹川バレバレになっててワラタ

「自衛隊へ外国人登用検討を」　笹川平和財団が小泉防衛相に提言 ★6 [煮卵★]
https://asahi.5ch.io/test/read.cgi/newsplus/1788426235/

ドワンゴ朝鮮人の仲間だっけ
三笠宮宮朝鮮人とエプスタイン、伊藤穰一も笹川グループ

90年代に京都府の政治過程調べてたからわかるっていうかさ
その頃は全くわからなん謎だったんだけどさ

なんで裏千家がクソ偉そうに政治に介入してるかわからなかったわけよ

クソダニ伊藤穰一絡みか
今わかったわ
またこいつら笹川三笠宮w
同じだわなIUTと

AIが完全自動でフェルマー最終定理を形式化。end-to-end。Claudeで11日間。
https://www.anthropic.com/research/formalizing-fermats-last-theorem
正しく証明された主要な定理は全て１年以内に自動で形式化されるだろう。

IUTは？

ダメだしされた

>>859

望月は子供とダメ出しされた

Faltings「僕らは子供のような学生達を受け持っており彼らを放り出すことはできないんだ。」

scholzeは数学の実在を書き表し小平数学も同様だ。
一方、望月IUTはabc予想の「証明」ほしさの妄想と連呼を表しIUTのlean形式化はハッキングによる正当化にすぎないだろう。
目指せコラッツ予想の偽証明か、、

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

IUTキチガイ朝鮮人の精神疾患メモw
こいつほんとなんもわかってない

ランダムウォークのスレ
https://rio2016.5ch.io/test/read.cgi/math/1787798247/

自己同一視が進んで
IUT理論の栄誉と自分の名誉が一体化してる人間がいるんだな
IUT理論が幻だと分かって発狂するのも当然でもともと狂ってる
強化子の喪失でそれが顕になったわけだ

>>880
朝鮮人朝鮮人って連呼して差別用語書き連ねながら日本人教授も嫉妬で叩きまくってるヘイト常習犯って五毛中共漢人か、小粉紅の中国漢人？

>>882
ワラタ
朝鮮人偽右翼の発言っすかw

>>240
中間発表はSSは間違ってるって主張には熱心だったが
PRIMSの査読は適切だったかどうかについては語ってなかったな

LANAは中立かもしらんが公正でもないな

望月はふんぞり返って事態を傍観してる場合じゃないだろ
数学者生命をかけて自ら率先して手を動かし汗をかき尽力しろよ、何様のつもりなんだよ
と言いたくなる

態度は大事じゃないからね

>>886
説明できないおっさんの末路だせえw

>>887
そうか

>>887
どうしてほしいと思ってるのかな

>>889
とっとと退場
税金使うな私費でやれ

>>885
とりまきに囲まれた裸の王様、、

ナビエストークスもおちたか

AIがミレニアム懸賞問題の一つ
ナビエストークス問題を解いた
話題ですか

-

AI Has Solved One of Math’s $1 Million Millennium Prize Problems

quanta magazine
2026年9月8日

https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/ppl

ナビエストークスのやつは性質調べるだけって
言ったらなんだけど
勘とHPCでいけそうな気もするが
LEANのところはLLM強いんだろうな
数日で結果出せる

一方、、

はよAIにknotの完全分類やって欲しいね

何を持って完全分類と呼ぶかになる
もう同値性の判定アルゴリズム自体はある
そこから先なんか面白い分類定理(有限単純群のときみたいな)こんなやつの全体で尽くされるのようなリストが作りうるかどうか
双曲型やザイフエルト型のリストアップくらいはできそうだけど
もう同値生判定アルゴリズムができた時点であんまり発展性は感じない

>>894
AIって名目なら金、計算資源が出せるってのは大きい

>>894
物理でも数学でもないパラダイムシフト
した望月IUTならハレーションおこして
カーネルを通過するかもしれませんね、

>>898

追加
>>231

IUT論文について共同通信記者からケドラヤへ質問。
PRIMSの受理と査読について
(ケドラヤはlean形式化もIUTもど素人).

1時間11分頃から

https://m.youtube.com/watch?v=2jgBBw6XjQ4&ra=m

　

>>894
君はLANAって全くわかってないよね。

age

>>901
え？知ってるけどw
IUTおじさんクソレス入れんなよゴミ

類体論の解析学を使う証明はLEANを通せるのかな？

楽勝です

kevin buzzardによる局所的.大域的類体論のleanによる形式化プロジェクトは、現時点で類体論が部分的に形式化された。

・主要な主定理（高木・アルティンの相互法則など）をすべて穴「公理化」がなく完全に証明しきるには至っていない、mathlibも同様だ。

・leanによる形式化は L関数など解析的方法を迂回しより容易な代数的方法に置き換えることも必要だろう

フェルマー定理のlean証明はできたらしいから類体論の証明体系も完成したと思ってたが違うのか

>フェルマー定理のlean証明はできたらしい

フェルマーの最終定理は証明された。
leanにより完全に形式化されたのか？
カーネルを通過したからOKになった
のか？

>>909
自分で調べればいいじゃん
https://github.com/anthropics/fermats-last-theorem

leanによる類体論の形式化についてだが、

FLTの証明でleanによる形式化に
必要な類体論の部分に限り　形式化したのでありscholzeの懸念の視点
からも検証が必要だ

>>910
あなたは調べたの？

>>912
調べてないよ。

・scholzeの懸念
　>>40

・Xena
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

IUTキチガイ、ランダムウォークスレ作ってクソ漏らすの巻

https://youtu.be/4JPLTOYoqXI?si=wo1Z_joispUSOCrb

AIって問題は解けるけど新しい理論とか手法は作れるんけ

重力理論と装置をつくってみた(螺旋重力 Spiral gravity)
https://rio2016.5ch.io/test/read.cgi/sci/1745635184/


IUTと双璧のキチガイ朝鮮人研究

ほらな
北朝鮮在日だろ？

「永遠の敵対はない」笹川陽平・日本財団名誉会長がロシア訪問　日露関係改善に意欲 　(産経) [少考さん★]
https://asahi.5ch.io/test/read.cgi/newsplus/1789864420/

>>914

lean3から入れ子構造機能など
を加えたlean4は健全性の証明が
未証明らしい。


➖
・コラッツ予想の偽.反証の証明

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

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

https://arxiv.org/html/2403.14064v2

>>920
追加

https://qiita.com/kyamaz/items/7b38e5977dc97747d2d9

伊藤穰一/笹川/マクスウェル/エプスタインラインな
ちなみにイスラエル建国当時の国民の半分がソ連人

「永遠の敵対はない」笹川陽平・日本財団名誉会長がロシア訪問　日露関係改善に意欲 　(産経) [少考さん★]
https://asahi.5ch.io/test/read.cgi/newsplus/1789864420/



で、こいつらと仲良いっていうか一心同体なのが
旧満州北朝鮮在日わんごおおおおおおおw

lean3から入れ子構造機能など
を加えたlean4は健全性の証明が
未証明らしい。

健全性の証明が未証明ってどこにそんなことかいてあるん？

>>921

>この結果は Lean3 のものです。
Lean4 では型理論が拡張されており（入れ子の帰納型、構造体に対する 規則など） Carneiro 自身が後の論文で「2019年の健全性証明はもはや直接には適用できない」と述べています

ほんまやね。まぁそのうち証明されるやろけど。たぶん純理論的には問題ない。一部残ってるかもしれないヒューマンエラーが洗い出されれば安心して使えるでしょ。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とか興味ない