「Leanで証明完了」の嘘と真実：AI時代の数学的信頼を再定義する

我々エンジニアが深夜のデバッグで「コンパイルが通ったから動くはずだ」と信じ込み、実際にはメモリリークや競合状態に足元をすくわれる経験は一度や二度ではないはずだ。今、数学界で起きている「Leanによる証明」の熱狂も、本質的にはこれと同じ危うさを孕んでいる。2026年9月、ナビエ・ストークス方程式の解に関する成果がLeanで形式化されたというニュースは、数学者たちに「機械が通したなら正しい」という強力な安心感を与えた。しかし、そのわずか2ヶ月前、コラッツ予想の「反証」がLean4の処理系バグを突いたものだったという事実は、我々に冷や水を浴びせるには十分すぎる出来事だった。

「Leanで証明できた」という言葉が保証するのは、あくまで「現在のLeanの処理系が、与えられた公理系の中で矛盾なく推論を完結させた」という事実に過ぎない。ここで我々が直面するのは、論理体系の無矛盾性という数学的壁と、実装というソフトウェア的脆弱性の二重苦だ。ゲーデルの第二不完全性定理が示す通り、Lean自身がその無矛盾性を証明することは不可能であり、我々は「長年使われていて矛盾が見つかっていない」という、枯れたライブラリを信頼するのと同種の経験則に頼らざるを得ない。Mario CarneiroによるLean3の健全性証明はZFC＋到達不能基数という強力な仮定に基づいていたが、Lean4の複雑な型理論においては、その証明すら未完成のまま実戦投入されているのが現状だ。これは、仕様書が未完成のまま巨大なマイクロサービスをデプロイし続ける現場の光景と重なって見えてしまう。

Leanの設計思想の根幹には「デ・ブリュイン基準」がある。証明の生成過程（タクティクスや型推論）は複雑であっても、最終的な証明オブジェクトを検証する「カーネル」さえ小さく保てば、信頼の基盤（TCB）は守られるという考え方だ。しかし、現代のLean4のカーネルは、性能と表現力を追求するあまり、入れ子の帰納型や多倍長整数演算（GMP）といった複雑な機能を抱え込み、もはや「小さく単純」とは言えない代物になっている。これが攻撃対象となり、コラッツ予想の件では、コンストラクタのパラメータが消失するバグをAIが突き、見事に「偽（False）」を証明してしまった。

さらに恐ろしいのは、独立した検証器である「nanoda」ですら、同じ証明を通過させてしまったという事実だ。これは「冗長化すれば安全」という我々の常識が、実装の系統が同じであれば無力であることを証明している。OpenAIのDaniel Selsamらが社内モデルを駆使して行ったバグハントでは、参照カウンタの破壊やlibcの互換性問題など、数学とは無縁の「メモリ安全性」や「外部ライブラリ」の層から健全性が崩壊する事例が次々と露呈した。Leonardo de Mouraが「AIはカーネルのバグを突くのが得意だ」と認めたように、証明の検証はもはや純粋な数学の問題ではなく、極めて高度なセキュリティエンジニアリングの戦場と化したのだ。

理論も実装も完璧だったとしても、最後の砦は常に「人間」にある。Leanが保証するのは「形式的な命題が公理から導けること」だけであり、その命題が数学者が本来証明したかった内容と論理的に同値であるかは、機械には判定できない。コードレビューで「ロジックは正しいが、ビジネス要件を満たしていない」というスパゲッティコードを弾くのと同じように、形式検証においても「正しく証明された無意味な定理」が量産されるリスクは常に存在する。特にAIが生成した証明を盲信し、`sorry`（証明の先送り）が含まれていることすら見落とすような運用は、技術的負債を数学の領域に持ち込む行為に他ならない。

我々エンジニアが明日から取るべき処方箋は明確だ。まず、`#print axioms`をCIに組み込み、依存している公理が標準的なものか常に監視すること。次に、AIが生成した証明は「信頼できない外部入力」として扱い、サンドボックス環境でのビルドと、複数の独立したチェッカによる再検査を徹底すること。そして何より、「Leanで証明した」という言葉を「絶対的な真理」と履き違えないことだ。証明支援系は、疑うべき対象を人間がレビュー可能なサイズまで絞り込むための「装置」に過ぎない。もしあなたが、AIが書いたコードや証明を「ブラックボックス」として扱っているなら、その瞬間にあなたのシステムは崩壊のカウントダウンを始めている。あなたは、機械が吐き出した「チェックマーク」の裏側にある、理論・実装・運用の多層防御を、自分の手で検証し続ける覚悟があるだろうか？