Anthropicは9月4日、AIアシスタント「Claude」を使い、17世紀に提示され1994年に英国の数学者アンドリュー・ワイルズが証明したことで知られる「フェルマーの最終定理」について、コンピューターが機械的に検証できる形式言語「Lean」による完全な形式化証明を世界で初めて達成したと発表した。研究は、Anthropicの研究者ティエンイー・ポン氏がコロンビア大学の共同研究者らと開発した数学形式化プラットフォーム「Prove2Me」と、Claude Codeをベースにした複数エージェントによる並行作業の仕組みを組み合わせて実施された。数十体のClaudeエージェントが役割分担しながら11日間にわたりほぼ自律的に作業し、合計で60億トークン規模の出力を生成、最終的に1300万行を超えるLeanコードと、約2万9500件の中間定理を書き上げたという。この証明は、Lean標準の3つの公理以外に何の仮定も追加しておらず、未完成部分を示す「sorry」のような一時しのぎのプレースホルダーも一切含まれていないとしている。
フェルマーの最終定理をLeanで形式化する取り組み自体は、英インペリアル・カレッジ・ロンドンのケビン・バザード氏が2024年に呼びかけたコミュニティプロジェクトとして既に進んでいたが、証明の規模と複雑さから完了までには数年単位の時間がかかると見込まれていた。Anthropicによれば、当初はClaudeエージェントを個別に作業させただけでは、全体の進捗を見失い、互いの作業内容がかみ合わなくなる問題が生じたという。これを解決したのが、証明の各部分がどのように依存し合っているかを追跡し、エージェント間の作業を調整し、完成済みの成果物を他のエージェントが探して再利用しやすくする「Prove2Me」の仕組みだった。人間側の関与は最小限で、開発者のポン氏が「ヤコビアンをスキームとして扱うのを優先すべき」「モーデル・ヴェイユの定理を早めに片付けてほしい」といった大まかな方針を随時示す程度だったという。
この証明をレビューしたバザード氏は、専門家の予想よりはるかに短い期間で達成された「並外れた自動形式化の成果」だと評価している。証明を形式化することは、人間による見落としの可能性を排除し、数学者同士が成果を共有しやすくする利点があるとされる。Anthropicは証明のコード一式をGitHub上で公開しており、今回の手法が現代数学の膨大な論文群を自動的に形式化していく道を開く可能性があるとしている。
