私たちは、フェルマーの最終定理の最初の完全なコンピューター検証済み証明を共有します。Claudeは11日間にわたり、ほぼ自律的にLeanプログラミング言語で証明を書く作業を行いました。以下では、形式化がどのように行われたかを説明し、この作業が研究数学にとって何を意味するかについての考えを共有します。

1637年頃、ピエール・ド・フェルマーは、ディオファントスの『算術』の自分のコピーの余白に、史上最も有名な数学的予想の1つとなる主張を書き留めました。すなわち、n > 2 のとき、aⁿ + bⁿ = cⁿ を満たす正の整数 a、b、c は存在しないというものです。この予想はフェルマーの最終定理（FLT）として知られるようになり、証明が非常に難しいことが判明しました。最初の証明は、サー・アンドリュー・ワイルズが1995年に発表し、129ページに及び、検証に数か月の骨の折れる作業が必要でした。

10年後、オランダのコンピューター科学者ヤン・ベルグストラは、ワイルズの証明を「形式化」することを提案しました。数学的推論をコンピューターが自動的に検証できる形式に変換することです。それ以来、数学者たちは、このような複雑な証明をエンコードするために必要な方法を開発してきました。2024年にロンドンのインペリアル・カレッジのケビン・バザードが開始した、Lean証明アシスタントを使用して形式化を完了するための複数年にわたるコミュニティの取り組みも含まれます。

最近、Anthropicの研究者であり、コロンビア大学のグループがAI形式化のためのツールを構築しているTianyi Pengは、ClaudeがFLTの形式化で進歩できるかどうかをテストすることにしました。結果は彼の期待を超えました。11日間、ほぼ自律的に作業し、ClaudeはFLTの最初のエンドツーエンドのコンピューター検証済み証明を生成しました。その過程で、1,300万行のLeanコードを書き、29,500の中間定理を証明しました。