9月4日、Xena Projectが「FLT: Anthropic has beaten me to it」と題した記事を公開した。AnthropicのAIがフェルマーの最終定理（FLT）の形式的証明を定理証明支援システムLeanで完成させ、数学形式化コミュニティ20年来のベンチマークをついに完結させたことが詳しく報告されている。
記事を書いたのはインペリアル・カレッジ・ロンドンの数学者Kevin Buzzard氏だ。Leanによる数学の形式化推進を目的としたXena Projectを主宰し、EPSRC（英国工学・物理科学研究会議）から100万ポンドの助成を受けて5年計画でFLTの形式化に取り組んでいた。その当事者が「Anthropicに先を越された」と綴ったのが本稿の主旨である。
フェルマーの最終定理とその「形式化」とは
フェルマーの最終定理は「$n \geq 3$ のとき $a^n + b^n = c^n$ を満たす正の整数の組は存在しない」という命題で、1637年にフェルマーが提示し、ワイルズが1995年に証明するまで約350年間未解決だった。その証明をコンピュータが検証可能な形式（Lean言語）で記述する作業が「形式化（formalization）」と呼ばれる。人間が書いた証明を機械が一行ずつ厳密にチェックできる状態にすることで、証明の正確性を原理的に保証できる。
Anthropicは内部モデル（詳細は公開されていないがClaude系列の研究用モデルとみられる）を用い、定理証明の共有・検証プラットフォームprove2.me上でFLTの完全な形式的証明をLeanで実装した。これは数学者Freek Wiedijnが定めた「形式化すべき100定理」リストの最後の1本だ。このリストは2000年代初頭から数学形式化コミュニティの非公式なロードマップとして機能してきたもので、その空白を埋めることで20年越しのベンチマークがついに完結したことになる。
11日間・1,340万行のコード
GitHubで公開されたリポジトリによれば、コードベースは1,340万行超に及ぶ。FLTの証明は楕円曲線・モジュラー形式・ガロア表現など現代数論の広範な理論を動員するため、Leanの数学ライブラリMathlibを大量に参照する構造となっており、コンパイル時間はMathlibの約20倍、96コア・500GB RAMのマシンでも相当な時間を要する。Buzzard氏はAnthropicの環境でコードを動かし、検証ツールcomparatorで確認した結果、証明が正しいと結論づけた。
所要期間はわずか11日間。Buzzard氏は「Anthropicが私より多くのお金を使ったかどうか気になるが…」と皮肉交じりに記している。
形式化されたのはどのバージョンの証明か
Anthropicが形式化したのは、1995年のDarmon–Diamond–Taylor論文によるワイルズ–テイラー–ワイルズ論法の解説版だ。Buzzard氏自身が取り組んでいる「より現代的なアプローチによる証明」とは異なる路線である。
技術的な補足として、この証明は**$p \geq 17$ の素数に対してのみ**FLTを示す形となっている。ただし奇数の正則素数の場合はBest・Birkbeck・Brasca・Rodriguezらがすでに形式化済みであり、最小の不規則素数は37であるため、全体として証明は完結している。
数学的新発見ではなく、「自動形式化」の可能性の証明
Buzzard氏は「この成果が数学的に新たに何かを教えてくれるわけではない。FLTの証明が正しいことは99.9%確信していたし、数論コミュニティのほとんどは100%確信している」と明言する。
しかし、この形式化が示す本当の意義は自動形式化（autoformalization）の実現可能性にある。Buzzard氏はこう述べる。
何千ページもの数学文献を、AIの群れが11日間でエンドツーエンドで形式化できるなら、将来は現代の研究成果がリアルタイムで形式化されるようになる。機械がラングランズ・プログラムを検証し、不完全な論証を容赦なく指摘する時代も来るだろう。また、「専門家には知られている」として仮定されている結果を重要な定理の証明がどれだけ使っているか、明らかになる。
ラングランズ・プログラムとは、数論・代数幾何・表現論を統一的に結びつけようとする現代数学の巨大な研究指針であり、FLTの証明もその成果の一部を活用している。査読プロセスの省力化や証明の透明性確保など、数学研究の構造的な変化への期待が込められた発言だ。
数学史の瞬間に二度とも居合わせなかった男
記事はユーモアあるエピソードで締められている。ワイルズが1993年にケンブリッジのニュートン研究所でFLTの証明を発表した際、大学院2年生だったBuzzard氏は第1回の講演を聴いたが「まったく理解できず」、残り2回をパスしてアイルランドへ恋人と旅行に出かけた。戻ってきてから定理が証明されたと知ったという。
今回も同じ展開だった。Anthropicからのメールはウェールズの音楽フェスティバル「Green Man」に同じ恋人と出かけている最中に届き、電波の悪い中で「End-to-end Lean formalization of Fermat's Last Theorem」というタイトルを一目見て「どうせ変な人だろう」と読み飛ばした。1,000通近い未読メールを処理しながら帰宅して、ようやく事態を把握したという。数学史の瞬間に二度も居合わせながら二度とも現場を離れていた、という自己観察が印象的だ。
詳細はFLT: Anthropic has beaten me to itを参照していただきたい。
