Anthropic、フェルマーの最終定理の形式的証明を公開：Claudeが完遂

Anthropicは、フェルマーの最終定理をLean 4で完全に形式化し機械検証したリポジトリ「fermats-last-theorem」をGitHubでオープンソース公開した。29,511個の定理と1,450個の定義モジュール、1300万行を超えるコードで構成される、史上最大規模のLean証明成果物となる。

フライ、セール、リベット、ワイルズ、テイラー＝ワイルズによる古典的な証明ルートを完全に網羅しており、Apache 2.0ライセンスで提供されている。ローカルブラウザで閲覧可能なインタラクティブ文書も同梱されている。

どのように構築されたか

本プロジェクトのLeanコードは人間が直接書いたものではなく、既存のオープンソース成果物を土台にAIエージェントが生成し、Leanの型検査システムを判定器として反復構築された。人間が読むことではなく機械検証を通すことを最優先しているため、変数名などはパイプライン由来の識別子となっている。

厳密性は極限まで保たれている。コードベース全体でsorryや追加の公理、native_decideなどのショートカットは一切使用されておらず、Leanが標準で備える3つの公理のみに依存している。

検証は二重に行われた。公式のLeanカーネルによるリプレイとコンパレータによる照合をパスしただけでなく、Rustで書かれた独立カーネルnanodaにも環境全体を渡して検証を実施した。nanodaは1,052,234件の宣言を検証し、ノーエラーで完了した。

動かし方と必要スペック

手元で完全にビルドを再現するには、LinuxまたはmacOSの高スペック環境が必要となる。パス長の問題からWindowsには対応していない。

ハードウェア要件は非常に重い。Lakeによるソースからのビルドは、並行ジョブあたり約5GBのメモリを消費し、96スレッド並行時のピークメモリは153GBに達する。ビルド時間は約5時間32分で、途中で生成される一時Cファイルだけで200GB以上のディスク容量を食う。その後の検証スクリプトには最大300GBのRAMと約15時間が必要となる。

証明の道筋を追いたいだけであれば、全体をリビルドする必要はない。リポジトリに含まれる約390MBのhtmlフォルダを展開し、ブラウザでindex.htmlを開くだけで、定理の依存関係グラフや定義をオフラインで閲覧できる。

なぜ重要か

形式手法の研究者や数学者、AIエージェントによるコード生成を追うエンジニアにとって必見の資料といえる。人間が何年もかけて手動で行ってきた長大な形式化作業を、AIと証明支援系コンパイラの組み合わせで一気にやり遂げられることを実証した。

機械生成されたコードは人間が読む教科書としては難解極まるが、ハルシネーションを原理的に排除した科学的推論基盤として、形式的検証の持つ決定的な強さを見事に証明している。