アンソロピック（Anthropic）は2026年9月4日、フェルマー最終定理（Fermat's Last Theorem。以下FLT）を、証明支援言語リーン（Lean）で端から端まで形式化した、と研究記事で伝えました。クロード（Claude）のエージェント群が、既存の証明を機械が一行ずつ検査できる形へ書き直した、という説明です。以下は、同社の研究ページとバザード氏のブログ、公開リポジトリまわりの整理です。
中心は、新しい数学を見つけたことではありません。すでに人間が通した議論を、抜けのない形に書き直し、コンピュータが通したかどうかを見ることにあります。
FLTは、「2より大きい自然数の指数では、正の整数のべきの和が同じ指数のべきにならない」という主張です。アンドリュー・ワイルズ（Andrew Wiles）氏が1995年に正しい証明を発表し、リチャード・テイラー（Richard Taylor）氏との修正を経て受け入れられました。人間向けの証明は明らかな段を飛ばすが、リーンはその飛ばしを許しません。
インペリアル・カレッジ・ロンドンのケヴィン・バザード（Kevin Buzzard）氏が2024年に始めたコミュニティ形式化は、初期段階の設計だけでも86ページ規模で、年単位の作業が目安でした。アンソロピックの研究者ティエンイー・ポン（Tianyi Peng）氏は、クロードで進むかを試し、結果が想定を超えました。同社によると、エージェントは約11日で端から端までの形式化を終え、リーン約1300万行を書きました。途中で約3万300本の定理を証明し、最終証明では約2万9500本を使いました。
初期の試みは、局所では進んでも全体の状態を見失い、協調が崩れました。失敗分は、最終の決まりきった繰り返し以外の行（非ボイラープレート）の約7%に残りました。成功したのは、ポン氏らが作った協調基盤プルーブツーミー（Prove2Me）と、クロードコード（Claude Code）系の実行の枠組み（ハーネス）を組み合わせたあとです。定理の依存は一方通行のつながり図（有向非巡回グラフ）で持ち、文と証明をファイル分割し、自然言語の説明で再利用しやすくしました。
使ったのは、クロード・フェイブル5.1（Claude Fable 5.1）に近い内部の汎用研究モデルで、出力の単位（トークン）は約60億です。証明の道筋は、ワイルズの議論をダルモン（Darmon）・ダイヤモンド（Diamond）・テイラーの解説に沿って簡略化した線です。新しい定理の発見ではなく、既存線の形式化です。
成果物はギットハブ（GitHub）のanthropics/fermats-last-theoremに公開されています。リーンの標準公理は3つのみで、プレースホルダ（sorry）や追加公理はありません。コンパレータ（comparator）で、証明した文がマスリブ（Mathlib。リーンの主要な数学ライブラリ）側のFLT文と一致します。別の検査プログラム（カーネル）のナノダ（nanoda）での検査にも触れています。
バザード氏は同日のブログでリポジトリをコンパイルし、コンパレータを実行して通りました。数学として新しいことはほとんどなく、人間が読む動的な解説やマスリブへの取り込みは別仕事だ、と分けて書いています。コンパイルは時間がかかり、メモリも大きいです。
| 公表されている説明 | こちらで確認できていないこと |
|---|---|
| 約11日で端から端までのリーン形式化（アンソロピック） | 11日間の全エージェントログの公開再現、外部が同じ工程を同じコストで再実行した記録 |
| リーン約1300万行、最終で中間定理約2万9500本（同） | 行数・定理数の第三者による再集計定義の統一 |
| 出力の単位（トークン）約60億、内部モデル（フェイブル5.1相当の目安）（同） | 公開モデルでの同規模再現、実費の独立監査 |
| 標準公理3つのみ、コンパレータでマスリブ文と一致（同） | 中間定理の名前が意図どおりかを機械が保証すること（リポジトリ自身も限界を記す） |
| プルーブツーミー＋実行の枠組み、初期失敗が約7%（同） | 失敗キャンペーンの詳細な公開データセット |
| バザード氏がコンパイルしコンパレータが通った（クセナブログ） | 本稿執筆時点での、他多数の独立グループによるフル再ビルド一覧 |
| ナノダ等の追加検査への言及（アンソロピック／二次整理） | 読者環境でのナノダ再実行の一般化手順の簡略化 |
工程の速さやトークン量は、アンソロピック自身の説明です。リーン成果物が通った、という点は、バザード氏のコンパイル報告が独立の確認になります。
規格や安全論証の文書では、結論の命題だけを機械検査できる形にし、人が読む物語調の説明は後から足します。製造の設計変更では、変更が満たすべき条件を検査可能な文にし、レビュー時間を結論文の一致に寄せます。受託開発の受け入れでは、仕様の「満たした」を検査可能な条件に直し、デモ動画だけに頼らない確認にします。
アンソロピックが示したのは、FLTの既存証明をリーンで端から端まで形式化し、機械が検査できる形にしたことです。約11日・約1300万行・中間定理約2万9500本は同社の説明です。新しい数学の発見ではありません。バザード氏はコンパイルとコンパレータの通過を述べ、一方で人間向けの解説やライブラリ整備は別だと分けています。
