コラッツ予想のAI「反証」で何が起きたか
コラッツ予想とは、どんな正の整数から始めても、偶数なら2で割り奇数なら3倍して1を足す操作を繰り返せば必ず1に到達する、という未解決問題です。反証するには、1に到達しない数が存在することを示す必要があります。
2026年7月25日〜28日に起きたこと
sorry なしのコラッツ予想「反証」リポジトリを公開A soundness bug in the Lean kernel ( #14576 ) was reported and fixed during the week of July 27. ／ On July 25, Ramana Kumar published a repository containing a sorry -free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576 . We pushed a fix one hour after the report ( #14577 ). Joachim Breitner reviewed it and suggested improvements, and it was merged. New patch releases are out. — 発生から修正までの経緯に関する記述より
「sorry なし」が通用しなかった
Lean で証明を書くとき、まだ埋めていない箇所には sorry という印を置きます。sorry が1つも無いリポジトリは、埋め残しのない状態でチェッカーを通した体裁になります。だからこそ、公開されたものが sorry なしだったことに重みがありました。ポストモーテムも、この点を明示したうえで有効な証明ではないと述べています。
ところが今回は、その検査そのものに抜けがありました。チェッカーを通ったという事実が、証明の正しさを保証しなかったわけです。ここが今回の核心にあたります。機械検証は人間の見落としを潰す仕組みですが、機械の側の実装にバグがあれば、その保証は成立しません。
3日で見抜かれ、1時間で塞がれた
一方で、対応の速さも記録に値します。公開から3日後には別の研究者が問題の核を取り出し、False（偽）を証明できる最小例へ縮約して不具合報告を立てました。報告からわずか1時間で修正が出され、レビューを経て本体に取り込まれ、修正版の配布まで済んでいます。
異常が持ち込まれてから塞がるまでの時間で見れば、この分野の検証体制はかなり速く回っていると言えます。
Leanカーネルのバグはどこにあったか
技術的な中身に入ります。難しく見えますが、外していけない点は1つだけです。本来なら型検査すべきものが、検査の対象から消えてしまっていたということです。
バグ #14576 の要点
The bug: when the kernel eliminates a nested occurrence under an inductive type T with parameters Ds , and these parameters are phantom (not mentioned in constructor fields), they disappear from the generated auxiliary type and thus escape type checking. An ill-typed argument in that position could be used to make the kernel accept a proof of False . The bug is only reachable through metaprogramming, by sending the inductive declaration to the kernel directly. The frontend checks the arguments and catches the ill-typed term. This is an implementation bug, not a hole in Lean's meta-theory. — バグの技術的内容、到達経路、および位置づけに関する記述より
普通に Lean を書いている人には届かない
範囲を正しく捉えておく必要があります。このバグに到達できるのは、メタプログラミング（プログラムでプログラムを組み立てる書き方）を使って帰納型の宣言をカーネルへ直接送り込む経路だけです。人が Lean のコードとして書いた場合は、手前のフロントエンドが引数を検査し、型の合わない項（式のひとかたまり）をそこで捕まえます。
つまり、既存の証明が片端から崩れるという話ではありません。意図的に細工した宣言を送り込んだときにだけ開く穴でした。すでに形式化されている証明が一斉に無効になる、という事態は起きていません。
メタプログラミングを禁じても解決しない
議論の中では、こうした攻撃を書けないようメタプログラミングを制限してはどうか、という案も出ました。ポストモーテムはこれを見当違いだと退けています。
理由は設計思想にあります。人が書いた式を内部表現へ変換するエラボレータという層は、そもそも信頼されない前提で作られています。健全性を、信頼していない部品が悪い項を作らないでいてくれることに依存させるわけにはいきません。悪意ある人物はコンパイル済みファイルを直接書いたり、メモリを書き換えたりしてエラボレータを丸ごと迂回できます。だからカーネル自身が、自分のプロセスの中で型の合わない宣言を拒まなければならない、という結論になります。関心事を層で切り分けて隔離できること自体が、証明項という方式の主な利点だとポストモーテムは述べています。
One suggestion in the discussion is to remove or restrict metaprogramming so that this attack is not expressible. This is misguided. The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker who wants to submit a malicious proof can also write .olean files directly or modify memory, both of which bypass the elaborator entirely. The kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns is one of the main advantages of proof terms. — メタプログラミング制限案に対する見解より
独立検証器も同時にすり抜けた
この件でとくに重いのは、実は本体のバグそのものではありません。保険として使われていた独立の検証器 nanoda（ナノダ）も、同じ証明を通してしまったという点です。
2つの実装で別々のバグが噛み合った
| 検証器 | 実装 | 今回の挙動 |
|---|---|---|
| Lean 公式カーネル | 参照実装 | 入れ子帰納型の検査が欠けていた |
| nanoda | Chris Bailey 氏による Rust の独立実装 | その箇所は検査したが、射影（構造から要素を取り出す操作）の型名を確認していなかった |
| lean4lean | 参照実装の移植 | 公式カーネルと同じバグの影響を受ける |
The original Collatz repository also passed a week-old version of nanoda , the main external checker. nanoda is an independent kernel (aka proof/type checker) for Lean implemented in Rust by Chris Bailey . The surprising part is that there are two unrelated bugs involved. The official kernel had a missing check in the nested inductive type support, as explained above. nanoda did check that spot, but did not verify the type name in a projection node. The nanoda bug was reported by Jeremy Chen and fixed a week before the Lean bug was reported. ／ The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both. ／ lean4lean is affected by the kernel bug, since its handling of inductives is a port of the reference implementation. — 独立検証器 nanoda がすり抜けた理由、独立カーネルによる検証が依然有効である理由、および lean4lean への影響に関する記述より
二重チェックは無効になっていない
独立カーネルによる検証は、今も有効です。今回すり抜けたのは、2つの無関係なバグがたまたま噛み合ったからで、片方だけでは通りませんでした。すり抜けるには2つの実装それぞれに別々の欠陥が必要だった、という事実はむしろ二重チェックの価値を示しています。
ただし条件が付きます。両方を最新版に保っていること。nanoda 側のバグは Jeremy Chen 氏が報告し、Lean のバグが報告される1週間前には修正済みでした。今回通ってしまったのは、1週間前の古い版で検証していたためです。証明を検証器に通す運用をしているなら、検証器のバージョン管理が保証の一部になります。
nanodaの穴を狙った時期の一致は偶然か
不気味なのは、狙われた箇所が「古い nanoda なら受け入れる式」だったことです。この点について Ramana Kumar 氏は、時期の一致は偶然だと考えつつも、モデルが nanoda の報告を見ていた可能性は否定できないとしています。Joachim Breitner 氏は別の見方を出しており、このバグを見つけられるだけの強力なモデルが手に入るようになったことが、時期の一致の理由ではないかと述べています。
The proof was built so that the expression the kernel never inspects is one that the old nanoda accepted. ／ Ramana believes the timing was coincidental, but cannot rule out that the model had seen the nanoda report. Joachim proposed the hypothesis that the timing coincidence is due to the availability of strong models able to find this bug. — 証明が狙っていた箇所、および時期の一致についての当事者の見解より
この件の後にLean側が変えたこと
ポストモーテムは反省で終わらず、実施済みの対応を列挙しています。この一件は防御を厚くする方向に働きました。
回帰テストとカーネルの追加検査
まず、今回の攻撃と、Arthur Adjedj（アルチュール・アジェジ）氏が指摘した関連ケース（非一様パラメータと呼ばれる別の形）について、回帰テスト（同じ不具合の再発を機械が検知する試験）が Kernel Arena に入りました。同じ穴が再び開いたら機械が気づきます。
続く修正 #14582 では、入れ子で現れるパラメータについて、型検査をやり直すだけでなく、実際にパラメータとして振る舞っているかどうかをカーネルが確かめるようになりました。加えてカーネルが常に保つべき前提条件そのものも強化されています。実際の変更点は公開されているので、修正の前後を並べて確かめられます。
無料ツールテキスト差分比較2つのテキストの差分をハイライト表示。変更点を素早く発見できます。今すぐ使ってみる →
Regression tests for the exploit, and for a related non-uniform-parameter case raised by Arthur Adjedj, are in the Kernel Arena . ／ A follow-up PR ( #14582 ) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them. ／ We have also hardened kernel invariants. PRs: #14621 , #14631 , #14632 . — 回帰テスト、追加検査、およびカーネル不変条件の強化に関する記述より
OpenAIの協力でさらに複数のバグが見つかった
見逃せないのがここです。OpenAI の Daniel Selsam（ダニエル・セルサム）氏が、サイバーセキュリティに特化したAIを使って Lean の開発組織 Lean FRO を支援し、カーネルの別の実装ミスを複数発見しました。いずれも修正済みで、6件の変更として反映されています。
この結果には続きがあります。新しく見つかったバグは、すべて nanoda が捕まえられるものでした。そして、これらもまたメタプログラミング経由でしか到達できません。前の節で見た「2つの実装が同時に外す確率は低い」という構図が、ここでも成り立っています。
AIがバグを作り、AIがバグを見つける。同じ週の出来事として並べると、この技術がどちら側にも効くことがよく分かります。数学の証明にAIを使う流れ自体は、Fable 5 がヤコビアン予想に取り組んだ件のように加速しています。
そしてこの nanoda は、同じ週に公開されたOpenAI Astra の未解決問題10問でも登場します。公開された証明を第三者が確かめるための手順に、nanoda が組み込まれているためです。穴が見つかったばかりの検証器が、そのまま次の成果の裏取りに使われているという関係になります。だからこそ、前の節で見た「両方を最新版に保つ」という条件が実務的に効いてきます。
Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed. All of them were caught by nanoda. These bugs are also only reachable through metaprogramming. PRs: #14607 , #14608 , #14609 , #14613 , #14615 , #14616 . ／ comparator.live now runs nanoda by default, and nanoda is tracked daily so lean-eval and comparator stay current after upstream fixes. — OpenAI の協力による追加のバグ発見と、検証環境側の更新に関する記述より
検証済みカーネルの取り組みはまだ途中
もう1つ、状況を正しく知るための事実があります。Mario Carneiro（マリオ・カルネイロ）氏の lean4lean は、Lean の型理論を Lean 自身で形式化し、カーネルがその理論どおりに実装されていることを証明しようとする取り組みです。
ただし作業は進行中で、無矛盾性（矛盾を導けないこと）の証明は帰納型をまだ覆っていません。そして検証対象となる実装自体が、今回と同じバグを抱えていました。ポストモーテムは、この部分の検証を完了させようとした時点でバグは見つかっていただろう、としています。形式手法で守り切る構想は、まだ完成していないというのが現在地です。
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. — lean4lean による検証の進捗に関する記述より
まとめ：機械検証をどう信じればいいか
この一件が示したのは、機械検証が無意味だということではありません。機械検証の保証は、検証器の実装の質に乗っているという当たり前の事実です。sorry が無いことは「すべての段が検査を通った」を意味しますが、検査そのものが正しい保証は別に要ります。
実務として取れる構えは3つあります。1つ目は、独立実装の検証器を併用すること。今回すり抜けるのに2つの別々のバグが必要だった以上、この防御は効いています。2つ目は、その検証器を最新版に保つこと。古い版で通したことが今回の直接の原因でした。3つ目は、重い主張ほど検証環境の版まで込みで示すことです。
そしてもう一点。バグを突いたのもAIなら、別のバグを見つけたのもAIでした。証明を書く側でも検証を固める側でも同じ道具が効くという事実は、この分野の当面の姿を示しています。公開された修正を読むときは、どの検査が足されたのかを1行ずつ突き合わせると輪郭がつかめます。
