Anthropicが2026年9月4日、フェルマーの最終定理について、コンピュータが全行程を検証できる形の証明が完成したと明らかにしました。作業の大半を担ったのはClaudeで、期間はおよそ11日間。書き出されたLeanのコードは1,300万行に達し、最終的な証明には2万9,500本の補助定理が使われています。数学の新しい定理が生まれたわけではありませんが、証明を確かめる側の作業に、これまでとは桁の違う速度が持ち込まれました。
350年かかった証明と、その先にあった検証の壁
フェルマーが本の余白に書き付けたのは1637年ごろのことです。3以上の指数について、aのn乗とbのn乗を足してcのn乗になる正の整数の組は存在しない。書いてあることは中学生でも読めるのに、証明は350年以上見つかりませんでした。1908年には10万金マルクの懸賞金がかけられ、最初の1年だけで621件もの誤った証明が寄せられています。※賞金額は現在の貨幣価値でおよそ100万〜200万ドル（約1億6,000万〜3億1,000万円）。1ドル156円換算。
決着がついたのは1995年、Andrew Wilesによる129ページの論文でした。ただ、この証明もすんなり受け入れられたわけではありません。1993年の講演で発表された最初の版は、検証作業の途中で決定的な穴を指摘され、Wilesは1年をかけて元教え子のRichard Taylorとともに埋め直しています。129ページを読み解いて正しいと言い切るまでに、何人もの数学者が数か月を費やしました。
そこで浮上したのが形式化という考え方です。証明を機械が読める言語に書き直し、論理の穴を計算機に洗い出させる。人間向けの証明は「明らかに」で飛ばす箇所が山ほどありますが、証明支援系のLeanはその一歩一歩を要求します。フェルマーの最終定理については、Imperial College LondonのKevin Buzzardが2024年に立ち上げたコミュニティ主導のプロジェクトが進行中で、最初の段階を記述した設計図だけで86ページありました。年単位の作業になると見込まれていた仕事です。
11日間で1,300万行
きっかけを作ったのは、Anthropicの研究者であるTianyi Pengでした。Columbia Universityで形式化ツールを作ってきた人物で、Claudeがこの難題にどこまで食い込めるかを試そうとしたところ、予想を超えた結果が返ってきたという経緯です。
数字を並べると規模が見えてきます。11日間で生成されたLeanのコードは1,300万行。途中で証明された定理は3万300本にのぼり、そのうち2万9,500本が最終的な証明に組み込まれました。参照元となるMathlibは数学の証明を集めたコミュニティの中心的なライブラリですが、今回の証明はその5倍を超える分量です。Anthropic自身も、必要以上に長い書き方になっている可能性が高いと認めています。
証明の筋道はWilesの原証明そのものではなく、Henri Darmon、Fred Diamond、Richard Taylorによる簡略版の解説を土台にしています。人間からの指示は「スキームとしてのヤコビアンを優先で」といった大枠の助言が時折入る程度でした。出来上がった証明はLeanの標準的な3つの公理だけに依拠しており、定理の主張がMathlibの記述と一致しているかどうかも専用の照合ツールで確認されています。
なお、この成果はゼロから積み上げたものではありません。Buzzardのプロジェクトや、正則素数の場合を扱ってきたflt-regularの蓄積から部品を取り込んでいますし、Leanとmathlibそのものが数百人の数学者の手で育てられてきたものです。Buzzardは今回の証明を読んだうえで、AIによる自動形式化の成果物が他の証明の土台として使える強度に達した点を評価しています。
最初の試みは失敗している
順調に進んだ話ではありません。初期の試行では、エージェントたちが序盤こそ成果を出すものの、プロジェクト全体がどこまで進んだかを見失い、協調が崩れていきました。この失敗した作業から最終成果物に残ったのは、定型部分を除いた行数の7パーセント程度だとされています。
流れが変わったのは、Prove2Meという共同作業の基盤に切り替えてからでした。Pengらが設計した形式化向けのプラットフォームで、効いたのは3点です。まず、証明すべき定理の依存関係を有向非巡回グラフとして保持し、エージェントが次に手を付けるべき場所を判断できるようにしたこと。次に、定理の主張と証明を別ファイルに分けてコンパイルを軽くしたこと。そして各定理に自然言語の説明を付け、既に証明済みのものを検索して再利用できるようにしたことです。
裏側の構成はClaude Codeをベースにしたマルチエージェントの仕組みで、消費した出力トークンはおよそ60億。使われたのは社内の汎用研究向けモデルで、性能はClaude Fable 5.1に近い水準とされています。
数学の現場に何が起きるのか
形式化が現実的な時間で終わるようになると、査読の重さが変わってきます。新しい結果が正しいかどうかを人間が何年もかけて確かめる工程を、機械がある程度肩代わりできるからです。AIが生成した数学が増えている今、その検証コストは無視できない大きさになりつつあります。
規模の面でも、この手法は大型プロジェクト専用というわけではなさそうです。Anthropicの研究者が個人向けのClaude Maxプラン3契約だけを使い、Prove2Me経由で協調させた小さな実験では、ヴィノグラードフの3素数定理の形式化が3日で完了しています。相応の足場さえ用意できれば、一般的な契約の範囲でも主要な定理の形式化に手が届くという見立てです。
Claude自身にとっても、Leanを書くことは副次的な効果を生んでいるようです。新しい結果を証明する過程で部分的な形式化を並行させ、自分の仮説が筋の通ったものかを自前で確かめる材料にしている、という観察が共有されています。数値シミュレーションを書いて方向性を確認するのと似た使い方です。
完成した証明はGitHubで公開されており、証明の流れを追える解説も添えられています。
まとめ
11日間、1,300万行、2万9,500本の補助定理。フェルマーの最終定理について、機械が端から端まで検証できる証明が初めて形になりました。新しい数学が生まれたわけではなく、価値があるのは検証の側です。証明の正しさを確かめる工程が人手から機械へ移りつつあること、そしてその成果物が次の証明の土台として使える強度を持ち始めたことが、今回いちばん大きな変化だと言えそうです。
