OpenAI、Astraが生成した10件の数学的成果を発表、Lean 4証明書を独立再構築可能な形で公開

OpenAIは、社内版Astraが生成した数学および理論計算機科学の10件の成果を発表した。対象分野は、高次元球充填、符号理論、群論、算術回路計算量、量子並列反復、格子暗号、極値組合せ論に及ぶ。同社によると、まずモデルが論証を発見し、その後、人間が同じモデルとともに合計249ページの原稿へまとめ、最後にモデルが各論証をLean 4証明書として形式化した。

具体的な主張には、一般の高次元球充填に対する漸近上界をCohn–Elkies線形計画法の閾値まで改善したこと、非sofic群を構成したこと、Connesの剛性予想を否定する反例を提示したこと、permanentに対する算術式の下界 Ω(n⁴/log n) を証明したこと、ユークリッド最近ベクトル問題について n^(1/400) 近似困難性を示したことなどが含まれる。OpenAIはさらに、Erdősの極値グラフ理論に関する2つの問題を解決し、多色三角形Ramsey数について超指数的下界を得たとも主張している。

自然言語による解答だけを公開する場合とは異なり、`openai/ten-proofs`リポジトリには、10件に対応する`.lean`モジュールが用意されており、Lean 4.32.0、mathlib、Lakeのバージョンが固定されている。研究者はmathlib cacheを取得した後、`lake build All`を実行して、すべての形式化証明を再構築できる。また、誤った公理、未宣言の仮定、信頼できない近道が証明チェーンに紛れ込むリスクを抑えるためのComparatorチャレンジも用意されている。OpenAIは、これらの解法の探索に使用したtoken数をSol APIの料金に換算すると約2,000ドルに相当すると見積もっているが、Astraのweights、完全な探索trajectory、失敗sample、実際の計算量は公開していない。

Lean kernelが証明書を受理することは、形式化されたstatementが指定された依存関係から導出可能であることを示すにすぎない。形式化された命題が元の公開問題と完全に同値であることを自動的に証明するものではなく、新規性や先行研究の確認に代わるものでもない。今後は、各分野の研究者が独立して再構築できるか、定義を照合できるか、さらに早い先行成果を発見するかが焦点となる。それまでは、この10件の成果は、machine-verifiable artifactを伴う重大な研究上の主張として扱うべきであり、peer reviewを完了した確定的な結論とみなすべきではない。