It shows a concrete, verifiable path (Lean-certified proofs) for validating AI-generated mathematical reasoning on problems that had stalled for a decade, which matters for anyone evaluating frontier model reasoning capability or building formal-verification-backed AI research workflows.
Key quotes
“Today, we are sharing a selection of ten results, each of which resolves or makes substantial progress on a long-standing open problem. These problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics.”
openai.com
“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.”
openai.com
“Multicolor Ramsey numbers. A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.”
openai.com
“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.”
openai.com
“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.”
