Claudeは11日間で1300万行を生成、60億出力トークンを使用
アンソロピックの研究記事によると、Claudeは1300万行のLeanコードを生成した。最終的な証明へ到達する過程で3万300件の定理を証明し、そのうち2万9500件を完成した証明で使っている。
Claudeが作成したLeanコードは、Mathlibの5倍を超える規模だ。Mathlibは、Leanを使って数学を形式化する際に利用される主要な数学ライブラリーで、すでに形式化された定義や定理を収録している。
完成した証明は、Leanが標準で認める3つの公理だけを使って検証された。専用の比較プログラムも、Claudeが証明した定理の内容がMathlibに登録されているフェルマーの最終定理の記述と一致すると確認した。
Claudeは11日間の作業で約60億の出力トークンを使った。出力トークンは、AIモデルが生成する文章やコードの量を数えるための単位だ。
API料金で換算すると、出力分だけで約4590万円
使用したモデルはアンソロピックの社内研究版で、同社はClaude Fable 5.1とおおむね同等としている。Claude Fable 5.1の公示API料金では、出力100万トークン当たり50ドル（約7650円）だ。
60億出力トークンにこの単価を当てはめると、出力分だけで約30万ドル（約4590万円）になる。
APIでは入力トークンやキャッシュから読み出すデータにも別料金がかかる。Claude Fable 5.1では、出力トークンの単価は入力トークンより高い。ただし、アンソロピックが自社モデルを動かす実際の原価と、顧客へ請求するAPI料金は同じではない。
したがって、約30万ドル（約4590万円）はアンソロピックが実際に支払った金額ではなく、公示API料金を60億出力トークンに当てはめた概算である。それでも計算規模をつかむ目安にはなる。
約30万ドル（約4590万円）は、93万4043ポンド（約1億9423万円）というバザードの助成総額の約24％、ほぼ4分の1に相当する。バザードが約5年間かけて使う研究費の4分の1近い金額に相当する出力が、11日間で発生した計算になる。
人間による数学上の指示は、大まかな方向づけに限定
数学者がClaudeへ与えた指示も限定されていた。人間側では、Tianyi Pengが時折、数学上の大まかな方針を示した。
PengのProve2Meは、定理同士の依存関係を示す有向グラフを使い、複数のClaudeエージェントによる作業を調整した。複数のClaudeエージェントは、証明すべき定理の関係をたどりながら作業を分担した。
新しい数学を発見したのではなく、既知の証明を機械で検証
アンソロピック自身も、今回の成果を新しい数学的発見とは位置づけていない。同社が新しい点として挙げるのは、人間向けに書かれた証明をLeanが確認できる形へ変換し、証明全体をコンピューターで最後まで検証したことである。
アンドリュー・ワイルズは1994年にフェルマーの最終定理を証明している。2026年9月4日に新しい数学上の答えが見つかったわけではない。
フェルマーの最終定理の形式化に長年取り組んできたバザードも、「数学的には、アンソロピックのこの仕事は本質的に何も教えてくれない」と書いている。
今回のコストが重要なのは、まさにこの点だ。11日間の大規模な計算は、新しい数学的知識を発見するためではなく、すでに知られている証明をコンピューターで確実に検証できる形にするために使われた。
