アンソロピックは米国時間2026年9月4日、AIモデルClaudeを使い、フェルマーの最終定理の証明を11日間でLeanに形式化し、コンピューターで検証できる状態にしたと発表した。作業では約60億の出力トークンを消費した。
フェルマーの最終定理そのものは、アンドリュー・ワイルズが1994年に証明している。今回の成果は新しい数学的発見ではない。重要なのは、すでに知られている証明を、人間の信頼に頼らずコンピューターで検証できる形にするため、膨大な計算資源が使われたことだ。
この事例は、AIが答えを作るためだけでなく、その答えが正しいかを確認するためにも大量の計算資源が必要になり得ることを示している。AI向けデータセンター需要を考える上でも、これまで十分に織り込まれてこなかったコストになる可能性がある。
5年計画で進める数学者に、Claudeが11日で先行
ケビン・バザードはインペリアル・カレッジ・ロンドンで、フェルマーの最終定理をLeanで形式化するプロジェクトを率いている。英国の工学・物理科学研究会議（EPSRC）が研究費を助成している。
ここでいう「形式化」とは、人間向けに書かれた数学の証明を、コンピューターが扱える厳密な形式に書き換えることだ。Leanは、その形式化された証明に論理的な誤りがないかを自動で検証するソフトウェアである。
英国の公的助成記録によると、バザードのプロジェクトには93万4043ポンド（約1億9423万円）が交付され、期間は2024年9月から2029年9月までとなっている。
2026年9月4日、アンソロピックは、Claudeが11日間でフェルマーの最終定理を形式化し、Leanによる検証まで終えたと発表した。バザードは自身のブログに反応を投稿した。
「私は5年間のプロジェクトに100万ポンド（約2億794万円）の助成を受けた。アンソロピックはわずか11日だが、使った金額はむしろ多かったのではないかとも思う……」
バザードの疑問には、公表されているトークン数とAPI料金から、おおよその費用を計算できる。
