OpenAIは10件の解探索に約30万6000円、既知の証明の形式化は約4590万円
OpenAIは2026年8月1日、数学と理論計算機科学における長年の未解決問題10件について、新しい成果を公表した。それぞれの問題を解決するか、大幅な進展をもたらした成果で、すべてに機械検証可能なLean証明書が付けられた。
OpenAIによると、10件の問題で解を見つけるためにモデルが使ったトークンをSol API料金で換算すると、総額は約2000ドル（約30万6000円）だった。
高くつくのは、答えを見つけることより検証できる形にすること
数字を並べると違いが際立つ。OpenAIでは、10件の未解決問題で新しい成果につながる解を探すための推定トークン料金が約2000ドル（約30万6000円）だった。
フェルマーの最終定理では、数学界が約30年間受け入れてきた既知の証明をコンピューターで検証可能な形に書き換えるため、出力トークンだけで約30万ドル（約4590万円）相当を使った。
高くつくのは答えを見つける工程ではなく、答えを作った人物を信用しなくても、コンピューターが正しさを確認できる形にする工程だ。
数学上の「発見」はほぼ無料に近づきつつあり、多額の計算資源が必要になるのは「証明」の側である。
AI向け計算資源の需要は、答えを作る処理だけでは決まらない
AI向け計算資源の需要予測は、主にAIが何かを「生成する」仕事を想定している。利用者の質問に答える、AIエージェントがコードを書く、人間が読む文章をモデルが作る、といった処理だ。
フェルマーの最終定理の事例が示したのは、AIが答えを作るための計算とは別に、答えを機械的に検証できる形へ変えるためにも大量の計算が必要になるということだ。
今回の形式化に必要だった計算量は、同じ数学問題についてモデルが通常の回答を生成するだけの場合に想定される計算量を大きく上回った。
企業では、増え続けるAI出力を人間だけで確認できない
企業で生成AIの本格導入が進まない理由にも、AIが作った内容をどう検証するかという問題がある。
MITのNANDA研究チームによる調査では、企業による生成AIの試験導入の95％が、損益に測定可能な効果をもたらしていなかった。大半の組織は、生成AIを試験段階から本番運用へ移せていなかった。
本番導入を妨げる決定的な要因が、モデルの性能不足であるケースは少ない。AIが回答を生成できても、回答が正しいかを確認する方法がなければ、企業は本番業務で安心して使えない。
AIが作る文章やコードの量は急速に増やせる。人間による確認作業を同じ速度で増やすことはできない。AIの出力量が拡大するほど、人間だけに依存した確認作業が先に限界へ達する。
