10月9日、Thomas Halesが「What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI」と題した記事を公開した。著者はピッツバーグ大学のThomas Hales教授で、ケプラー予想の証明で知られる数学者であり、形式証明分野の第一人者だ。本稿はテレンス・タオのブログへのゲスト投稿として公開されたものである。

2026年9月、Anthropicがフェルマーの最終定理をわずか11日間・1300万行のLeanコードで自動形式化したと発表した。同月、OpenAIはNavier-Stokes方程式のブローアップ解の形式化を発表している。数学の「形式証明」がAIに委ねられる時代が急速に到来しているが、その基盤となる証明検証システム「Lean」そのものの信頼性が、まさにその同じ夏に揺らいでいた。2026年7〜8月、Leanのカーネル（証明チェッカー）に「健全性バグ」が相次いで発見されたのだ。Halesの記事はこの問題の全容と対策を数学者向けに整理したものである。

「Lean健全性バグの夏」——2026年に何が起きたか

健全性バグとは、証明カーネルが「False（偽）」の証明を受け入れてしまうバグのことだ。Falseが一度でも証明できてしまえば、論理的にあらゆる命題が証明可能になる——形式証明システムにとって最悪の種類の欠陥である。

2026年7〜8月、Leanのカーネルに複数の健全性バグが相次いで発見された。その一つはコラッツ予想の「不正な反証」を生み出し、別のバグはHales自身が発見する形でケプラー予想の不正な短証明を生成した。さらに2025年5月には整数オーバーフローに起因する健全性バグも報告されていた。

ただしHalesは「これは災害ではなく、前向きな進展だ」と評価する。バグを発見したのは悪意ある攻撃者ではなく、セキュリティ研究者とフロンティアモデルAIの組み合わせだったからだ。

• コラッツバグを発見したのはRamana Kumar——検証済みML処理系「CakeML」の共著者
• 複数のバグを発見したのはOpenAIのDan Selsam。Lean開発者de Mouraのポストモーテムによれば、「AIがこれ以上の問題を発見できないと報告した時点で作業を終了した」という

発見されたバグはすべて修正済みで、Leanの数学ライブラリ「mathlib」（現在約250万行）も修正済みカーネルで再検証されている。

自動形式化（Autoformalization）が実用段階に入った

従来、数学の論文を形式証明に変換するには膨大な人手が必要だった。ケプラー予想の形式証明は約20人年の作業と50万行のコードを要している。2026年はこれがAIで自動化されるフェーズに突入した年だ。主なマイルストーンは以下の通りである。

• 2025年9月：Math Inc.（自動形式化に特化したスタートアップ）が素数定理の「準自動形式化」（人間の介入が必要な箇所あり）を実現
• 2026年1月：Josef Urban（チェコ工科大学）がMunkresのトポロジー教科書の大部分を2週間で13万行に自動形式化
• 2026年3月：Math Inc.が24次元球充填問題を自動形式化。約50万行を生成、コード削減後は約20万行
• 2026年5月：Meta/Facebook Researchが数学教科書26冊の大部分を自動形式化するプロジェクト「ATLAS」を発表
• 2026年9月4日：Anthropicがフェルマーの最終定理の自動形式化を発表。11日間で1300万行のLeanコードを生成
• 2026年9月8日：OpenAIがNavier-Stokes方程式のブローアップ（爆発解）の形式化を発表

さらに同日、Jared Lichtmanが「既知のすべての数学を形式コードに変換する」ことを目指すMAP（Mathematics Autoformalization Project）を立ち上げた。

Leanの信頼性をどう担保するか

LeanはCIC（Calculus of Inductive Constructions：帰納的構成の計算）と呼ばれる型理論に基づいている。数学者に馴染み深いZFC集合論との相互変換可能性はB. Werner（1997）の論文で理論的に示されており、両者の「橋渡し」が存在する。カーネル自体は数千行のC++コードで構成されており、コンパクトに保つことで検証可能性を高める設計だ。

健全性バグへの対策として、Halesは三つのアプローチを紹介している。

1. 複数カーネルによるクロスチェック
現在、約25のLean向け独自カーネルがLean Kernel Arenaにリストされている。Navier-Stokes形式化はすでに十数種類の証明チェッカーで確認済みだ。ただしコラッツバグの事例が示すように、クロスチェックだけでは完全ではない。別のカーネルが同様のバグを持っていれば見逃してしまう。

2. カーネル自体の形式検証
ゲーデルの第二不完全性定理により「バグゼロの証明」は原理的に不可能だが、相対的無矛盾性証明は目指せる。MLコンパイラを検証済みコードで実装したCakeMLや、Cコンパイラを形式検証したCompCertの成功例がある。

3. AIによる支援（ただし慎重に）
AIは健全性バグの発見に有効だった。しかし証明を読んでそれが正しいかを判断させる用途については、Halesは慎重な見方を示している。

形式証明を「信頼する」ための条件

Halesが最後に強調するのは、カーネルによる機械的な検証だけでは不十分だという点だ。定理の「ステートメント監査」——命題文がわれわれの意図した定理と一致しているかを人間が確認するプロセスが欠かせないという。

Navier-Stokes問題であれば、Leanの定義がFeffermanのミレニアム問題の記述と一致しているかを人間が確認しなければならない。LeanにはこのためのComparatorツールが用意されており、未許可の公理の混入チェックも行える。

1300万行のコードを11日で生成できる時代に、その内容を人間が精査するコストは逆説的に増大している。形式証明の「信頼性」は、AIの能力と人間の監査能力のバランスの上に成り立つ——Halesはそう示唆している。

詳細はWhat mathematicians should know about the Lean Theorem Prover: questions of reliability and AIを参照していただきたい。