9月7日、Nature が「Anthropic AI 'formalizes' proof of Fermat's last theorem in just 11 days（AnthropicのAIがフェルマーの最終定理の証明をわずか11日で「形式化」）」と題した記事を公開した。AnthropicのAIチャットボット「Claude」が、人間の数学者が10年かかると見込まれていたフェルマーの最終定理の形式証明をわずか11日で完成させたという。生成されたコードは1,300万行——この数字と日数の組み合わせが、数学・AI両コミュニティに衝撃を与えている。

人間が10年かかると見込んでいた証明を、AIが11日で

Anthropicは9月4日、高度なプロトタイプ版Claudeを使ってフェルマーの最終定理をコンピュータ検証可能なコードに変換したと発表した。生成されたコードは1,300万行に及ぶ。

「機械が数学者たちの仕事をこれだけ強固な証明に変換できるとは、完全に度肝を抜かれた」——ラトガース大学の数論研究者、Alex Kontorovichはそう語る。

フェルマーの最終定理とは、「nが2より大きい整数のとき、x^n + y^n = z^n を満たす正の整数の組 (x, y, z) は存在しない」という命題だ。フランスの数学者ピエール・ド・フェルマーが1637年に提唱したものの証明は残さず、350年以上にわたって未解決だった。1994年にアンドリュー・ワイルズとリチャード・テイラーがついに証明を完成させ、20世紀数学の金字塔となった（ワイルズは2016年にアーベル賞を受賞）。この証明はモジュラー形式と楕円曲線を結びつける「谷山・志村予想（現・谷山・志村・ヴェイユ定理）」を中心に据えた、きわめて高度かつ広範な数学的技法を駆使するものであり、その長大さと難解さゆえに形式化は困難とされてきた。

今回のAIの作業は、この証明を「形式化（formalization）」するものだ。形式化とは、人間が自然言語で書いた数学的な議論を、コンピュータが誤りなく検証できるコード——通常は定理証明支援系（proof assistant）である**Lean——に変換する作業を指す。Leanは一般的なプログラミング言語とは異なり、数学的証明の論理的正しさを機械的に確認することに特化したシステムだ。数学コミュニティでは、Leanを中心に証明の形式化ライブラリMathlib**が整備されており、形式化の重要性は近年急速に高まっている。証明の正しさを機械的に保証できるため、数学知識全体の信頼性担保という観点でも注目を集めている。

「1桁違う難易度だった」

今年2月にも、AIによる形式化のマイルストーンがあった。マリナ・ヴィアゾフスカがフィールズ賞を受賞した球充填問題（8次元・24次元空間における最密充填の証明）の形式化が完了したのだ。しかし今回のフェルマーの最終定理は、その比ではなかったと専門家は口をそろえる。

インペリアル・カレッジ・ロンドンの数学者Kevin Buzzardはこう語る。「おそらく1桁難しかった」。

トロント大学の数論研究者Daniel Littはさらに踏み込む。「フェルマーの最終定理を形式化できたなら、おそらく何でも形式化できる」。

数学の「誤り検出」装置としてのAI

この成果が示す先は、形式化作業の効率化にとどまらない。Buzzardは「2年前には夢物語だったことが、今は現実になっている」と述べ、AIが数学の文献全体を精査し、広く信じられてきた定理に誤りを発見する可能性すら排除できないとする。

数学の証明は長大で複雑なため、人間が見落とすミスが混入することがある。コンピュータ検証可能な形式証明が広がれば、Mathlibのような数学知識のライブラリ全体の信頼性を機械的に担保できるようになる。

なお、フェルマーの最終定理そのものの実用上の応用は乏しい。しかしワイルズが証明のために開発したモジュラー形式・楕円曲線にまつわる技法群は、整数論・代数幾何・数論幾何など数学の離れた分野をつなぐ架け橋となっており、その形式化によってこれらの数学的手法がより広く検証・活用されやすくなることが期待されている。

詳細はAnthropic AI 'formalizes' proof of Fermat's last theorem in just 11 daysを参照していただきたい。