Lean定理証明器の信頼性とAI、Hales氏が自動形式化の現在地を解説

形式化とLeanの歩み

形式化された証明とは、数学の基礎と論理の基本ルールのレベルまで網羅的に検証された証明を指します。手作業でも理論上は可能ですが、ステップ数が膨大になるため、通常は専用ソフトウェアを使って計算機で行います。これまでに四色定理、Feit-Thompson（奇数位数）定理、ケプラー予想、球面外反、8次元と24次元の球充填問題、ナビエ・ストークスの強制爆発、フェルマーの最終定理などが形式化されています。最後の3件は今年完了し、形式化の可能性への関心を広く集めました。

形式化用のソフトウェアは証明支援系、定理証明器、対話型定理証明器などと呼ばれ、本稿では同じ意味で使います。これまでにAutomath、HOL Light、Isabelle、Coq（昨年Rocqに改名）、Metamath、Mizar、Leanなどが開発されてきました。Freek Wiedijk氏は著書でこれらの一部を比較し、2の平方根が無理数であることの証明を各系で示しています。数学者の間で最も人気があるのはLeanで、2013年にMicrosoft在籍時のLeo de Moura氏が開発し、同社を説得してオープンソース化されました。

2017年にはJeremy Avigad氏の大学院生だったMario Carneiro氏がJohannes Hölzl氏とともに、Leanのコアライブラリから独立した数学ライブラリmathlibを立ち上げました。mathlibは現在、約30万の定理、10万を超える定義、250万行のコードを含み、700人以上の貢献者が関わっています。mathlib内の定義や定理は他の定理の証明に再利用でき、たとえばコーシー・シュワルツの不等式を使う証明では、それを再証明せずライブラリから引用できます。

自動形式化の到達点

従来、研究者は論文の証明を人手で形式証明に書き写す必要がありました。3次元の球充填に関するケプラー予想の形式証明は、完了までに約20人年を要し、約50万行の証明スクリプトからなります。自動形式化は、その労力を自動化する長年の夢の実現です。AIが論文（PDFやTeXファイルなど）を読み、Leanなどの証明支援系の形式証明を出力する仕組みを指します。

自動形式化は2026年に実用的な現実になりました。2025年後半から研究者の期待は高まり、いくつかの節目が報告されています。2025年9月にはMath Inc.が素数定理の「準」自動形式化を実現しましたが、AIが行き詰まるたびに人間が追加の指示を与える必要がありました。2026年1月にはJ. Urban氏が、集合論ベースの証明支援系でMunkresの位相テキストの大部分を2週間で13万行に形式化したとするプレプリントを公開しました。3月にはMath Inc.が24次元の球充填問題の自動形式化を発表し、約50万SLOCを生成したのち、コード削減で約20万行に圧縮しました。

5月にはMeta/Facebook ResearchのグループがATLASと呼ぶプロジェクトで26冊の数学教科書の大部分を自動形式化しました。9月4日にはAnthropicがフェルマーの最終定理の自動形式化を発表し、11日間で1300万行のLeanを生成しています。9月8日にはOpenAIが強制項付きナビエ・ストークス爆発を発表し、その定理のLeanによる自動形式化も併せて示されました。Urban氏は1月の時点で、どの証明支援系を使うかに関わらず自動形式化が2026年に容易かつ遍在的になるかもしれないと述べています。

Leanの土台と検証

Leanは型理論、とりわけCIC（calculus of inductive constructions、帰納的構成の計算）と呼ばれる型理論の一派に基づいています。1901年のラッセルのパラドックスは数学の基礎に危機をもたらし、その後10年で2つの解決策が提案されました。ひとつは危険な集合の生成を禁じるツェルメロの集合論の公理、もうひとつはラッセルのパラドックスのような対象の生成を構文エラーにする型理論です。型理論は1903年にラッセル自身が著書で導入しました。

集合論に慣れた数学者にとっては、B. Werner氏の1997年の論文「Sets in Types, Types in Sets」が安心材料になります。この論文は、ZFC集合論をCICに符号化でき、CICのある方言をZFC（到達不能基数の階層を加えたもの）に戻せることを示しています。型は互いに素な集合のようなもので、型理論の各要素はちょうど1つの型に属します。自然数2の型は自然数型、自然対数の底eの型は実数型であり、自然数型から実数型へは明示的な型変換が用意されています。

Leanは汎用プログラミング言語と数学言語が別々ではなく一体になったシステムです。プログラムコードとアルゴリズムの正しさに関する定理を混在させたり、プログラムで数学的証明を生成したりできます。Leanの証明スクリプトは解析され、elaboration（数学版のコンパイルのような処理）を経て、Leanカーネルによって検証されます。カーネルは数千行のC++コードで、慎重に設計されていますが極めて複雑です。

mathlibは約250万行のLeanコードからなり、elaborationを経てカーネルで検証されています。この250万行のどこかに無条件に偽の証明があれば、それはカーネルかランタイムが偽の証明を拒否できなかった責任です。したがってLeanの証明はカーネルで検証されるまで信じるべきではなく、さらに人間による監査で「検証された定理が意図したものか」「定義が想定と一致するか」を確認する必要があります。Leanのcomparatorツールがこの作業を補助し、不正な公理の検査なども行えるとされています。

健全性バグの夏

健全性バグとは、カーネルが「偽」の証明、ひいてはあらゆる命題の証明を許してしまうバグです。証明支援系にとって最も深刻な種類のバグであり、数学の信頼性を重視する数学者に警鐘を鳴らすものです。2003年、ヘイルズ氏は当時最も信頼できるカーネルとされたHOL Lightで健全性バグを発見しました。そのカーネルはわずか数百行のコードでした。Lean 4は2023年9月にリリースされ、リリース前に2件の健全性バグが見つかって修正され、2025年5月にはオーバーフローによる別のバグが報告されています。

2026年の春から夏にかけては「健全性バグの夏」と呼ばれる状況となり、7月と8月にLeanの複数の健全性バグが明らかになりました。この混乱は様々な証明支援系に及びましたが、本稿はLeanに焦点を当てています。あるバグはCollatz予想の不正な反証を可能にし、ヘイルズ氏自身もケプラー予想の短い不正な証明が生成されたことでこのバグを知りました。これらのバグはすべて迅速に修正され、mathlibは修正後のカーネルで検証済みだとされています。

ヘイルズ氏は、これらのバグの検出は前向きな展開だと見ています。バグを発見したのは悪意ある攻撃者ではなく、信頼できるカーネルに関心を持つセキュリティ研究者の手にあるフロンティアモデルのAIでした。Collatzのバグは、ML言語の検証済み実装であるCakeMLの共著者Ramana Kumar氏が発見しました。複数のバグはDan Selsam氏が発見し、de Moura氏の報告によれば、同氏はOpenAIでサイバーセキュリティに特化したAIをLean FROに提供し、カーネル内の他のプログラミング上の誤りも見つけたとされています。

残る注意点

カーネルは慎重に作られていますが極めて複雑で、基盤となる型理論に欠陥があれば、それがコードに実装されている限り深刻なカーネルの欠陥になります。証明がカーネルで受理されたとしても、記述の忠実性を人間が監査する必要があるという点は変わりません。ナビエ・ストークスの場合、Leanの記述がFefferman氏によるミレニアム問題の記述と対応するか、実数の体や偏微分、測度といった概念が正しく定義されているかを人間が確認すべきだとされています。

自動形式化で生成される証明の規模が大きくなるほど、この監査の重要性は増すと考えられます。本稿が示す範囲では、カーネルによる機械的な検証と人間による記述の監査という二段構えの必要性が強調されており、規模の拡大にこの体制が耐えられるかは今後の課題として残っています。