Claude、フェルマーの最終定理を11日で形式化

Anthropicは2026年9月4日、フェルマーの最終定理の初の完全なコンピューター検証済み証明を発表した。AIモデルのClaudeが、Leanというプログラミング言語で証明を書くために11日間ほぼ自律的に作業した成果だという。詳細はAnthropicの発表にまとまっている。

フェルマーの最終定理は、1637年に数学者フェルマーが書き残した予想である。証明したのはアンドリュー・ワイルズ卿で、1993年6月に3日間の講義で最初の証明を発表したが、2ヶ月後の検証作業で証明の重大な欠陥が指摘された。ワイルズが最初の正しい証明を発表したのは1995年5月で、その証明は129ページに及んだ。この証明は、人間の数学者が読んで検証することを前提に書かれている。その約10年後、オランダの計算機科学者ヤン・ベルフストラが、この証明を「形式化」する、つまり数学的な推論をコンピューターが自動で検証できる形に変換することを提案した。2024年には、インペリアル・カレッジ・ロンドンのケヴィン・バザードが、Lean証明支援システムを使って形式化を完了させる複数年のコミュニティプロジェクトを立ち上げていた。

コロンビア大学のグループを率いるAnthropicの研究者ティエンイー・ペンが、Claudeにこの形式化を進めさせられるか試すことにした。結果、Claudeは11日間で1300万行のLeanコードを書き、29500個の中間定理を証明し、最終的な証明を完成させた。作業には数十のClaudeエージェントが協働し、概念を定義し、中間定理を証明し、それらを使ってより難しい命題を証明するという積み上げ方をしている。1300万行という規模は、この定理が基盤とするMathlibという数学コミュニティの主要な証明ライブラリの5倍を超える。バザードは、この自動形式化の成果について、数学の公理以外の仮定なしにフェルマーの最終定理を証明するものだと評価している。

この形式化作業は当初、完了までに数年かかると見込まれていた。実際、初期段階を記述するためだけのブループリントが86ページに及ぶ規模の計画である。それが11日間で終わったという事実は、長時間にわたる地道な検証作業を、AIエージェントに任せられる範囲が広がっていることを示している。会議の議事録や打ち合わせの記録も、録音さえしておけば後からAIに任せられる作業の一つだ。メモリス（AIボイスメモ）は、録音した音声を渡すと数分後に文字起こしと要約が届く仕組みで、地道な書き起こし作業を人の手から外す発想は今回の話と地続きにある。

この成果を仕事の文脈に引きつけると、まず注目すべきは数十のエージェントが11日間協働したという体制そのものである。一つのモデルに一つのタスクを渡すのではなく、複数のエージェントが概念定義・中間証明・応用という役割分担のもとで並行して積み上げ、最終的に1300万行という一人の人間には見渡しきれない規模の成果物にたどり着いた。仕事の現場でAIを使うときも、単発の指示で一気に完成品を求めるより、小さな検証可能な単位に分解して積み上げさせる設計のほうが、長時間タスクでは成果を出しやすいという構造は変わらない。今回の11日間という期間も、無数の中間定理という検証可能な単位に作業を分解できたからこそ実現している。

これとは別に、この成果をどう受け止めるかにも注意がいる。Claudeが行ったのは、フェルマーの最終定理という新しい数学的発見ではない。すでにワイルズが1995年に証明し、人間の数学者コミュニティが正しいと認めてきた証明を、コンピューターが機械的に検証できる形へ変換する作業である。証明の正しさそのものは1995年の時点で決着しており、Claudeの11日間が短縮したのは「人間が読んで検証する」という工程を「コンピューターが自動で検証する」工程に置き換えるための翻訳作業の時間だ。この区別を曖昧にすると、AIが未解決の数学的難問を次々解いているかのような過大評価につながりかねない。今回の発表が示しているのは、新しい定理を発見する能力ではなく、既知の正しさを機械可読な形に落とし込む作業を高速化する能力であり、この二つを分けて見ることが、今後のAIによる数学研究の報道を読み解くうえでの実務的な指針になる。