AnthropicのAIがフェルマーの最終定理をLeanで形式化

Anthropicが、フェルマーの最終定理の完全な機械検証済み証明をLeanで書いて公開しました。同社によると、社内の研究モデルが11日間でこれを生成しました。出来上がったものは、形式化された数学の主要なオープンライブラリであるMathlibの約5倍の規模です。

Leanは証明支援系です。数学をコードとして書くと、kernelと呼ばれる小さなプログラムが一つひとつの手順を検査します。フェルマーの最終定理は、nが2より大きいとき、a^n + b^n = c^nを満たす正の整数a、b、cの組は存在しない、という主張です。Andrew Wilesが1995年に証明しました。しかしこれまで、計算機が最後まで検証できる形でこの証明を書き下した人はいませんでした。

リポジトリに実際に入っているもの

Anthropicの研究記事は2026年9月4日に公開されました。コードはGitHub上にApache 2.0ライセンスで置かれています。

READMEは形式的な定理を述べています。正の整数a、b、cと、3以上の任意のnについて、a^n + b^nがc^nに等しくなることはありません。

項目	数値
Leanツールチェーン	4.33.1
Mathlibリビジョン	v4.33.0
定理数	29,511
モジュール数	60,475
ビルド時間	96並列ジョブで5.5時間
メモリ最大使用量	230 GB
エクスポートサイズ	37.8 GB

READMEの記述のうち、規模よりも重い意味を持つものが2つあります。この証明にはsorryが含まれていません。sorryは、誰も完成させなかった手順を表すLeanのプレースホルダです。そして証明が依存する公理は3つだけです。propext、Classical.choice、Quot.soundの3つで、いずれもLean自身に同梱されています。議論を閉じるために追加で仮定したものはありません。

Anthropicによると、モデルが証明した定理は全部で30,300件でした。そのうち約29,500件が最終的な証明に入りました。同社は出力トークン60億、生成されたLeanコード1,300万行という数字を挙げています。作業はProve2Meを通して進みました。これは形式化を小さな命題に分割し、並列に動くエージェントへ渡すプラットフォームです。

証明がどう検査されたか

検査は3系統が別々に走りました。ここが理解する価値のある部分です。

最初にLean自身のkernelが証明を受理しました。次にcomparatorというツールのバージョン4.33.0が、約15時間かけて再検査しました。最後にNanodaが1,052,234件の宣言を約30分で検証しました。NanodaはRustで書かれた独立したkernelです。

Nanodaが重要なのは、Leanとコードを共有していないからです。Leanのkernelにバグがあっても、Leanのkernel自身はそれを見つけられません。別の言語による2つ目の実装は、その危険に対する本物の歯止めになります。

数学者はどう見ているか

Kevin Buzzard氏はXena Projectを率いています。同氏は英国の研究助成機関EPSRCから5年間で100万ポンドの助成を受け、まさにこの定理の形式化に取り組んでいました。同氏は自身のブログで、Anthropicが先に到達したと書きました。

Buzzard氏は結果を否定していません。「FLTの証明に問題がないことを99.9%確信している」と同氏は書いています。Anthropicのページでは、この成果を「並外れた自動形式化の達成」と評しています。

一方で同氏は境界線も引いています。この形式化は「証明に関する初期の文献に忠実に従っているだけで、何も付け加えていない」と書きました。Wilesの議論について、1995年のDarmon-Diamond-Taylorによる解説をなぞったものです。ここで新しい数学が見つかったわけではありません。新しいのは、古い数学が機械で検証できるようになったことです。

Buzzard氏は、この証明が17以上の素数を対象としていると指摘しています。それより小さい非正則素数は、すでに他の人々によって形式化されていました。同氏の記事へのコメント欄で、David Jao氏はこの実行のAPI費用をおよそ30万ドルと見積もっています。

これが開発者にとって意味すること

Leanを書いているならリポジトリをクローンできますが、先にハードウェアを確認してください。96ジョブで5.5時間のビルドと230 GBのメモリ最大使用量は、ほぼすべてのノートPCを除外します。代わりに生成済みのHTMLドキュメントを読んでください。390 MBあり、ビルドは不要です。

応用できる教訓は、モデルが1,300万行を書いたことではありません。誰もその行を読まずに済んだことです。kernelが数分で正しさを判定しました。それを生成したものを信頼する必要はありませんでした。

これは検査器が存在する場所でしか成り立ちません。Leanには検査器があります。あなたのWebサービスにはありません。これを型紙として使う前に、自分のスタックで何がkernelの役割を果たすのかを考えてください。型システム、プロパティテスト、ファジングツールが通常の候補です。

AIが書いたLeanをレビューするなら、機械的な確認2つで大半を賄えます。sorryを検索すること、そして公理の一覧を出力することです。Anthropic自身の主張はこの2つの事実に乗っており、どちらも自分で安く確認できます。

最後に目を引くのは費用の差です。証明の生成には11日と数十億トークンがかかりました。別の言語での再検証には30分しかかかりませんでした。Anthropicは以前にも研究モデルを実験室の作業に向けており、ここでも同じ型が当てはまります。生成は高くつきます。検査は安上がりです。