OpenAIのAstraが数学の未解決問題10件を前進させ、証明も公開

Today, we are sharing a selection of ten results, each of which resolves or makes substantial progress on a long-standing open problem. ／ The results were achieved by an internal version of Astra, our next major model. The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates. These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate — 導入段落および "The results" 節の、成果の位置づけ・成果を出したモデル・探索に要した費用・作業の流れに関する記述より

These problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. ／ Multicolor Ramsey numbers. A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183. ／ Extremal number conjectures. Results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180. ／ discovered while evaluating an unreleased model. This work has already inspired further developments in mathematics and theoretical computer science ／ Subsequent research includes Bloom, Sawin, Schildkraut, and Zhelezov ／ an initiative providing 100,000 scientists and mathematicians with free access to our best ChatGPT models. We also continue to evaluate our models on open research problems during development. — 対象分野の列挙、表に挙げた成果のうち多色のラムゼー数と極値数の予想の記述、5月の反証と脚注の後続研究、研究者向けの取り組みに関する記述より（残る成果も同じ一覧に併記されている）

This repository contains Lean 4 formalizations of the results presented in ／ The project uses Lean 4.32.0, mathlib, and Lake. ／ Apache-2.0 license — 公開リポジトリの位置づけ、ビルド環境、およびライセンス表記より

Afterward, the model formalized each argument in a Lean certificate — 形式化の作業に関する記述より

Independent proof checking ／ For instructions on checking the formalizations with Comparator, see the — リポジトリの README にある独立した証明の検査の案内より

We believe attribution should honestly reflect how a result was produced: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work. We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness, while the mathematical arguments themselves were generated by our system. ／ The emergence of systems capable of contributing to mathematical research raises questions that cannot be answered by a technology company alone. There are many views as to the role of AI in mathematics, and we have deep respect and understanding for those concerned with its impact, including the signers of the Leiden declaration on AI and Mathematics ／ We hope the mathematical community will engage deeply with these results, place them in context, and bring the ideas behind them to life through new research and discovery. — 著者性と責任の所在、数学コミュニティへの姿勢に関する記述より