Anthropicは、Lean 4で書かれたフェルマー最終定理の完全な機械検証済み証明をApache 2.0ライセンスでオープンソース化した。コードは数学ライブラリMathlibの上に構築されている。リポジトリが示す形式的な命題は「任意のn≥3および正の整数a、b、cについて、a^n + b^n ≠ c^nが成り立つ」というもので、Lean上ではカーネルが1ステップずつ検証できる定理として記述され、証明に抜け穴は残されていない。
このプロジェクトで最も分かりやすいのは規模だ。リポジトリの集計によれば、モジュール数は60475、定理数は29511、定義用モジュールは1450にのぼり、エクスポート検証は1052234件の宣言をカバーしている。生成されたHTMLドキュメントは約390MB、完全なエクスポートファイルは37.8GBに達する。ローカルで一通り再現するには300GB超のディスク容量と、ピーク時で約153GBのメモリが必要になる。
3段階の検証、すべてに記録あり
リポジトリは「コンパイルが通った」という一言だけでは済ませていない。1段階目はLean 4.33.1自身によるカーネルの完全コンパイルで、96コアマシンで5時間32分を要した。2段階目はleanprover公式のcomparatorツール(v4.33.0)による再検証で、約14時間46分を要した。3段階目はRustで書かれた独立カーネルnanoda 0.4.13に切り替え、16スレッドで約30分、Your solution is okay!という出力を得ている。
3段階の検証に加えて、もう一つの厳格な制約がある。全モジュールにおいてaxiom、sorry、native_decide、unsafe、extern、implemented_by、partial def、#evalを一切使用しないことだ。これらのキーワードはLeanコミュニティで抜け穴として広く知られている。sorryは文字通り「ここはまだ証明されていない」ことを意味し、native_decideは一部の判定をカーネルが検証しない機械語コードに委ねてしまう。これらをすべて排除するということは、証明の信頼性をLeanのカーネルと検証ツールのみに委ねると認めることに等しい――README自体もそう説明している。
AIがどれだけ書いたかは、リポジトリも明かしていない
READMEの説明によれば、Leanのソースコードは「人間が書いたオープンソースのLeanコードの上で、Leanを審判役としてAIエージェントが生成した」という。具体的な比率は公開されていない。どのモジュールが人間によるもので、どのモジュールがモデルによって生成されカーネルに差し戻されて書き直されたものかという内訳は、公開資料からは読み取れない。
一方、人間が用意した土台については比較的明確に示されている。既存の学術プロジェクト由来の依存ファイルは106件あり、その大半はインペリアル・カレッジ・ロンドンのKevin Buzzard氏が主導するFLT形式化プロジェクトと、Kummerの正則な場合を扱うflt-regularによるものだ。これとは別に、Mathlibに既にある内容を再証明したモジュールも23件ある。
形式数学の歴史という文脈に置くと、今回の規模の飛躍は際立つ。四色定理は2005年にGeorges Gonthier氏がCoqで形式化を完了させ、ケプラー予想を扱うFlyspeckプロジェクトは2014年に完了が宣言された。いずれも人年単位の作業量だった。BuzzardチームがFLTプロジェクトを立ち上げた際も、外部の見立ては同様に複数年規模だった。今回のリポジトリがそのゴールをどれだけ前倒しにしたのかは、人間とAIの実際の分担比率次第であり、それこそが現時点で唯一公開されていない数字でもある。
参考資料：Anthropic公開リポジトリのREADMEおよび検証記録、CocoLoop、Mathlibプロジェクト、インペリアル・カレッジ・ロンドンのFLTプロジェクト公開資料。モジュール数、定理数、および3段階の検証所要時間はリポジトリの記載に基づき確認した。