Astraが数学・TCSの10難問で新結果、Lean証明も公開

AIによる科学支援は、コード作成や文献検索から、数学の新しい結果候補を生み出す段階へ踏み込んだ。OpenAIは2026年8月1日、未公開モデルAstraが数学と理論計算機科学の10件の長期未解決問題で新しい進展を示したと公開した。

今回の重みは数字にある。OpenAIによれば、解を見つけるまでの総token量をSol API料金で換算すると約$2,000だった。人間の研究者が長く取り組んできた問題群で、この規模の計算費用から新しい道筋が出たという主張は、数学コミュニティにとって無視しにくい。

対象は広い。高次元sphere packing、binary codeとspherical code、non-sofic groupの存在、Connes rigidity conjectureへの反例、permanent計算の算術回路・公式下界、一般two-player quantum gameのexponential parallel repetition theorem、格子暗号に関わるclosest vector problem、Ehrhart volume、multicolor Ramsey number、extremal graph theoryが並ぶ。

注目点は、論文風の文章だけで終わらせていないことだ。OpenAIは、Astraが生成した論証を人間が原稿として整え、その後モデルが各論証をLean certificateへ形式化したと説明している。さらに各解法についてreasoning walkthroughも出した。専門家が追跡し、反証し、修正できる材料を残した形になる。

もちろん、受け入れはこれからだ。OpenAIは正確性に責任を持つとしつつ、AIが生成した証明を通常の人間著者の成果として扱うのは実態を歪めるとも述べた。次に重要なのは、独立した数学者がLean certificateと原稿を読み、どの結果がそのまま通るのか、どこに補強が必要なのかを確かめる作業だ。