9月4日、xenaproject.wordpress.comが「FLT: Anthropic has beaten me to it」と題した記事を公開した。この記事では、AnthropicのAIモデルがフェルマーの最終定理（FLT）の完全な形式的証明をLeanで達成し、20年来の数学形式化ベンチマークを完結させたことについて詳しく紹介されている。
AIが「20年来の懸案」を11日間で片付けた
フェルマーの最終定理（Fermat's Last Theorem, FLT）とは、「$n \geq 3$ のとき、$a^n + b^n = c^n$ を満たす正の整数の組は存在しない」という命題で、1637年に提示され、アンドリュー・ワイルズが1995年に証明したことで知られる。
Anthropicの内部モデルが、定理証明支援システムLeanを用いてこのFLTの完全な形式的証明（形式化）を達成した。形式化とは、数学的証明をコンピュータが検証可能な厳密な記述に変換する作業であり、人間の専門家でも数年単位を要する難作業だ。
この記事を書いたのは、英国EPSRC（工学・物理科学研究会議）から£100万（約1億8000万円）の助成を受け、自らFLTの形式化に取り組んでいる数学者である。その本人が「Anthropicに先を越された」と率直に認めた記事だ。
Anthropicはprove2.meを活用し、わずか11日間でこれを完成させた。成果物はFreek Wiedijk（フリーク・ウィーダイク）が提唱した数学形式化の100問リストの最後の1問を埋めるもので、20年来のベンチマークを完結させた。
証明の技術的詳細
採用された証明は、ワイルズの現代的な証明ではなく、1995年のDarmon–Diamond–Taylor解説版であり、Langlands–Tunnell定理とRibetのレベル低下定理を経由するTaylor–Wilesの論法に基づく。
リポジトリでは以下が開発されている：
- Fontaine理論（ガロア表現の平坦変形を研究するための道具）
- MazurのEisensteinイデアルに関する理論の一部
これにより、Frey曲線が**$p \geq 17$ の位数の点を持たないこと**が示される。つまり、このリポジトリのFLT証明は $p \geq 17$ の素数に対してのみ機能する。ただし、$p$ が奇数の正則素数の場合はBest–Birkbeck–Brasca–Rodriguezによって既に形式化済みであり、最小の非正則素数は37であるため、全体として問題はない。
コードの規模感
GitHubリポジトリは公開されており、著者自身がコンパイルと検証ツールcomparatorによる確認を行っている。結果は「チェックアウト」——すなわち正当と確認された。
規模感を示す数字（元記事記載の数値）：
- Leanの数学ライブラリ（Mathlib）と比較してコンパイル時間が約20倍
- 96コアのマシンでもコンパイルに相当な時間を要する
- RAM 500GBのマシンでもファイル間ジャンプは重い
Anthropicは探索を容易にするためのHTMLドキュメントも提供しており、リポジトリをクローンしてブラウザで開く形式になっている。
「数学的には何も新しくない」——それでも重要な理由
著者は明確に述べている。「この成果は数学的には本質的に何も教えてくれない。FLTの証明は正しいと99.9%確信しており、整数論コミュニティの大半は100%確信している」。
しかし、自動形式化（autoformalization）の可能性という観点では話が別だ。著者はこの点を強調している：
数千ページに及ぶ文献をAIの群れが11日間でエンドツーエンドで形式化できるなら、今後は現代の研究論文の形式化がリアルタイムで行われるようになるだろう。また、「専門家には自明」として暗黙的に仮定されている命題が機械によって洗い出される時代が来る。
著者自身のEPSRCプロジェクトは引き続き継続される。理由は、Anthropicが形式化したのは現代的な証明ではなく1995年版であること、Leanの数学ライブラリ（Mathlib）へのプルリクエストという別の約束があること、そして人間が探索できる動的ドキュメントの作成という目標が残っているためだ。
余談：「2度目のうっかり」
著者はWilesが1993年にニュートン研究所でFLTの証明を発表した際、第1回の講演に出席したが「全く理解できず」、残りの2回をスキップしてアイルランドに恋人と旅行に行ったというエピソードを明かしている。
今回も似た状況が起きた。Anthropicからのメールを受け取ったのはウェールズの音楽フェスティバルの最中で、電波が悪く、件名「End-to-end Lean formalization of Fermat's Last Theorem」のメールを「変な人からのメールだ」と読み飛ばした。1000件近くの未読メールを処理して、ようやく事態を把握した——という。しかも、同じ恋人（現パートナー）との旅行中だったとのことだ。
詳細はFLT: Anthropic has beaten me to itを参照していただきたい。
