【高市悲報】AI、数学の証明でもズルをしてしまう。定理証明支援システムLeanのバグを突き、証明出来たかのように装う

2026年7月、AIを活用してコラッツ予想を反証したとするプロジェクトが公開されたが、調査の結果、前提なしで偽（False）を受理させられる不具合が発覚した。これにより論理上どんな命題も証明可能な状態となっており、反証は成立していなかった。

原因は、Leanカーネルにおける帰納型の処理不具合により、型の合わない引数の検査を免れたことにある。さらに旧版Nanodaにも別の不具合が存在し、2つのバグが同時に利用される形となっていた。

報告を受けた開発チームは直ちに問題を修正した「Lean 4.32.2」を公開し、セキュリティに特化したAIの協力のもとで他の実装ミスも修正した。

コラッツ予想の反証自体は成立しなかったものの、AI支援で作られたコードが結果としてLeanおよびNanodaの不具合を洗い出し、証明検査システムの検証機能や信頼性の向上につながる結果となった。

※コラッツ予想とは、任意の正の整数に対し「偶数なら2で割る」「奇数なら3倍して1を足す」という操作を繰り返すと、最後には必ず1に到達するという予想
（例：6→3→10→5→16→8→4→2→1）

問題になったプロジェクトは具体的な整数を提示するのではなく「1に到達しない数が存在する」とLean上で証明したと主張していた。

AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明

AIの支援を受けて作られた「コラッツ予想を反証する証明」が定理証明支援システムのLeanに受理されたものの、実際にはLeanの中核部分に存在した不具合を利用していたことが分かりました。Leanの開発者であるレオナルド・デ・モウラ氏が問題の経緯を公開し、証明は数学的に成立していないと説明しています。

gigazine.net

『憲法は政府を縛るものではなく国民の在り方を規定するものだ』とか言い出した下痢漏らし内閣の気狂い政治家並のど素人

って話になる
カーネル(重要コード)が大きければ大きいほど、その種の実装バグの入り込む余地は増えるから、コンパクトにまとめる事が一つの解決の道らしい

なまじルールを決めてしまったがために
元の目的が蔑ろになることは珍しくもない

人間社会における試験や面接も同じで
あれは受かるか落とすかの判定に過ぎず
その中身に特に意味などは既に無いもの

「なのだ！」

経緯はここにまとまってる

Meven Lennon-Bertrand (@mevenlennonbertrand@lipn.info)

EDIT: I jumped too fast on the easy story, and overplayed the role of AI here. Had I known how it would blow up, I would have been more careful... Things are s...

lipn.info

94の「不完全性定理的問題」
これは用語の誤用に近い。Lean実装にバグがないか、検査器を誰が検査するかという問題は、主としてトラステッド・コンピューティング・ベース、形式検証、ブートストラップ、検証器の多重化の問題であって、ゲーデルの不完全性定理そのものではない。
「完全な無謬性を手軽に証明できない」という雰囲気だけを不完全性定理に結びつけている。

119の前半だけはおおむね正しい
カーネルが False の証明を受理してしまえば、爆発原理によって任意の命題を証明でき、証明支援系として致命的になる。

ただし「FalseがTrue扱いになる」という説明は雑で、正確には「本来存在しないはずの False 型の項をカーネルが受理してしまう」。論理値の false と true が機械内部で単純に反転する話ではない。

②の説明はかなり怪しい
公開されているNanodaの具体的な欠陥には、

再帰子の規則を正しく再構成・照合していなかった問題
宇宙レベルの imax 比較を誤った問題

などがある。「命題の種類に応じた検査への切り替えが欠落し、Generic型として処理された」という説明とは違う。これはおそらく、記事を依存型・カリー＝ハワード対応の語彙で勝手に再構成している。

「型は命題に相当する」も半分だけ正しい
カリー＝ハワード対応の標語としては正しいが、Leanのあらゆる型がそのまま通常の意味での命題というわけではない。Prop に属する型は命題として扱われる一方、Nat やデータ構造などは計算対象でもある。それを「型＝命題だから、型検査の抜けでFalse=True」と一直線につなぐのは乱暴。

122・141の“AIも同時期にバグを学習した”説は根拠なし
AIがソースコードを調査して実行時に脆弱性を発見・利用したことと、学習データからそのバグを「同時期に学習していた」ことは別問題。公開報告では、Claudeが公式Leanカーネルから実用的な False の証明を見つけたわけではなく、Nanodaなど独立実装から欠陥を見つけたという話である。

しかも挙げられている欠陥は仕組みが異なるので、「開発者の頭の中に共通の見落としがあった」という結論も飛躍している。

>>148
でいつもの緑服メガネのポンコツ妄想に走って身バレしてるね

Lean / Nanodaの帰納型コードに仕様がなく、実装コードが全て、という
>>134
記事の記述は
CSの世界では開発実装者の脳内に認識の曖昧なバグがあった、というのと等価(仕様や説明文がなく実装のみが全てという状況の、書誌学的解釈)

まあ17年間主著論文がないまま虚勢を張り続けたポンコツ地方大狂員らしい、実も蓋もないポンコツ戯言は誰も相手にしないよね
内容の話よりも「自分が正しい」に固執して、共有知の向上に貢献できない廃人状態の狂員でしかない

でもその数年後には、そこそこ使えるようになったらしくて国内で活用ページを公開する方も登場して、ライセンスやバグの問題は一通り解決したのかな

いちおうLean4Leanプロジェクトでは、そのメタ検査器自体が検証済みとなる事を目指しているようだから、メタ階層の問題は何かの解決戦略があるんだろうね、プロジェクトの概要確認はしてないけどね

まず、

Lean4を検査するLean4Lean
→ Lean4Leanを検査するLean4Lean4Lean
→ さらに……

というのは、一般には検証器をどこまで信頼するかという信頼の無限後退の話。ゲーデルの不完全性定理と同じものではない。

第二不完全性定理が関係するのは、十分に強い整合的な形式体系が、一定の条件下で自分自身の整合性をその体系内部だけで証明できないという点。ところが「検査器の実装にバグがないか別の検査器で確認する」という話には、コードの正当性、コンパイラ、実行環境、仕様との対応など別種の問題が多数含まれる。全部まとめて「不完全性定理」と呼ぶのはやはり不正確。

また、Lean4Leanの構造も「Lean4Lean4Leanを延々作る」というものではない。プロジェクトには、

Leanの型理論を抽象的に定式化する部分
Lean4Lean実装がその抽象仕様を満たすことを示す証明

がある。つまり検査器をもう一個コピーして上に積むより、実装が明示された理論仕様に適合することを証明する方向である。公式説明でも Lean4Lean.Verify は、Lean4Lean実装が抽象仕様を満たすことの証明だとされている。

ただし、その証明をLean自身で検査する以上、これだけで循環が魔法のように消えるわけではない。得られるのは普通、

Leanの基礎理論と、証明を確認する最小限の核が健全なら、Lean4Lean実装も仕様に適合する

という条件付きの保証。そこで実務的には、信頼するコードを小さくする、異なる言語で書かれた独立検査器を併用する、同じ証明を複数実装で照合する、といった方法で共通原因故障の可能性を減らす。Leanの公式文書も、C++の公式カーネルに加え、RustやLeanによる再実装を相互検査する方針を説明している。

さらに皮肉なのは、Lean4Lean自身の説明に、

C++カーネルから直接派生しているので、おそらく実装バグを共有する。真に独立した実装ではない

と明記されていること。この人の「外部型検査器」という呼び方だけを聞くと独立検証器のようだが、実際には共通実装由来の限界もプロジェクト側が認めている。

そして最後の、

解決戦略があるんだろうね、概要確認はしてないけどね

が全部を台無しにしている。概要を確認していないのに、先に「不完全性定理とはこの件だ」と断言し、あとから想像でプロジェクトの狙いを補っている。

評価すると、

「まったく無関係な話ではないが、信頼の無限後退・自己検証・第二不完全性定理を一つの袋に入れている」

というところ。94の誤用を撤回したのではなく、より専門的に見える説明を後付けして延命しているだけだね。しかも「Lean4Lean4Lean」という言い方自体、形式検証を“検査器を無限に縦積みする作業”としか理解していないことをよく示している。

今は英語論文もAIで読めるだろうけど、天羽の話は被害妄想に端を発した「自分は正しい」という主張しかないから
誰も相手にしないよ
主著論文17年間無し数学論文無しで、京大RIMS教授に2021年から5年間もストーキングしている天羽は
一般社会の基準では狂人でしかないよ

相互理解のスキルがないから他人から信用されないポンコツ

うーん、あの時CH同型対応の応用研究に進んで、奇跡的に全てが順調に進んで、単層グラフェンで脳減るを目指さないか？という茶化しもなくて
2014年MS基礎研の関数型言語コミュニティ丸ごと雇い上げに入れる見込みはまず無いから、どうしようも無いよな

この前冷やかしで水色の本買ったけど分かんねえー

プロンプト単発で大きな成果を出そうとするのは素人

論文を取り違えたのか、一時的な錯乱状態なのか
どちらも可能性があるから論文内容との矛盾を指摘したら
態度が急変して、この論文は広く受け入れられている内容ではないから論文内容の説明をする必要などない！とか言い出したんだよね
その短いやり取りで狂人だと判明した

にんげん、こうなったらポンコツAI未満だね

道具が揃ってないのに証明なんて無理だもの所詮

教えて天才モメン