OpenAI says its next major AI model can do more than answer difficult questions — it can help produce new mathematics.
The company announced Saturday that an internal version of its next major model, dubbed Astra, generated solutions to ten longstanding open problems across mathematics and theoretical computer science. The topics ranged from quantum complexity and high-dimensional sphere packing to lattice cryptography and group theory, with every targeted question left unresolved for a decade or more.
To back up its claims, OpenAI released a 249-page collection of manuscripts alongside computer-verifiable Lean 4 proof certificates on GitHub. Notably, the repository’s “sorry” count—the indicator used in Lean when a proof step is left unproven—stands at zero, confirming that the compiler verified every logical step.
The compute cost to generate the raw tokens for all ten solutions came out to an estimate of $2,000 at GPT-5.6 Sol application programming interface rates.
Machine reasoning meets mathematical rigor
The headline discovery is an explicit construction of a non-sofic group, resolving a fundamental question in group theory that has lingered since mathematician Mikhail Gromov introduced the concept in 1999. Astra also produced a counterexample to Connes’s rigidity conjecture concerning group von Neumann algebras, proved Ehrhart’s volume conjecture, and settled three items from Paul Erdős’s famous problem catalog, including problem 183 on multicolor Ramsey numbers.
OpenAI noted that while Astra performed the underlying mathematical reasoning, human researchers worked the model’s outputs into formal papers suitable for publication. Afterwards, the model formalized each argument into Lean code.
Tension at the human frontier
Despite the automated verification via Lean, none of the ten findings have undergone traditional academic peer review yet. Human mathematicians must still confirm that the formalized statements accurately map to the original open questions and evaluate the broader significance of the findings.
The announcement comes during growing friction between tech firms and academic institutions. The International Mathematical Union endorsed the Leiden Declaration in June, which warns that AI developers risk eroding standards around proof, consent, and scientific credit. Furthermore, public access to Astra remains pending, as the system must clear a newly established federal AI safety review process in the United States before launch.
The economics of automated discovery
Beyond the theoretical progress, Astra points toward a dramatic shift in the economics of scientific research. Solving ten historic mathematical problems for the price of a mid-tier laptop demonstrates that deep academic reasoning is quickly becoming a cheap commodity.
When high-level problem-solving costs thousands of dollars instead of millions in research grants, the primary bottleneck in science shifts from generating breakthrough ideas to human validation. Tech firms and research institutions will soon need to adapt to an environment where machines churn out complex theoretical frameworks faster than human experts can evaluate them, forcing a fundamental rethink of academic publishing, research budgets, and intellectual property.
Read more: OpenAI’s confidential IPO filing signals its next phase of enterprise growth and channel partner expansion.