On August 1, OpenAI announced that an internal version of its next model family, Astra, solved ten open problems in mathematics and theoretical computer science. The company published a 249-page manuscript alongside machine-checkable Lean 4 certificates for every result on GitHub. The computational cost for all ten solutions was approximately $2,000 at current API rates.
The results span group theory, operator algebras, combinatorics, high-dimensional geometry, quantum complexity, and circuit theory. The headline result is the first explicit construction of a non-sofic group, resolving a question that had stood since Mikhail Gromov introduced the concept of soficity in 1999. Astra also disproved Connes's rigidity conjecture on von Neumann algebras, proved Ehrhart's volume conjecture, solved three problems from the Erdős catalogue including Problem 183 on multicolored Ramsey numbers, and improved the general upper bound on high-dimensional sphere-packing density for the first time since 1978.
The Verification
Two results carry implications beyond pure mathematics. Astra proved exponential parallel repetition for every finite two-player entangled quantum game, a foundational result in quantum complexity theory. A direct reduction from 3SAT established polynomial-factor hardness of approximation for the closest vector problem. Lattice problems like the closest vector problem form the mathematical foundation of most post-quantum cryptographic systems. Stronger hardness results mean stronger theoretical security guarantees for the encryption designed to survive quantum computers.
The Lean certificates are the unusual part. Lean 4's trusted kernel gives a binary verdict: the proof compiles or it does not. No committee deliberates. No reviewer requests revisions. Fields Medalist Tim Gowers said he would have recommended the earlier Erdős unit distance disproof for publication in a top journal "without hesitation." Thomas Bloom, who maintains the Erdős problems database, called the August results "big news" and more significant than the May result.
The Declaration
In September 2025, sixty researchers and policymakers gathered at Leiden University and produced what became the Leiden Declaration on Artificial Intelligence and Mathematics. The International Mathematical Union endorsed it. The declaration warned against using published research without consent, bypassing peer review, and announcing results through press releases rather than submitting them to journals. It flagged threats to proof attribution and the integrity of mathematical publishing.
OpenAI announced the Astra results through a blog post. The company published reasoning walkthroughs and Lean certificates but submitted nothing to any journal. Sebastien Bubeck, OpenAI's head of mathematics research, described the results as "beautiful" on social media. Noam Brown added: "Sadly, no Millennium Prize Problems (yet)." Gary Marcus called the achievement "amazing but vastly oversold."
The Cost
The $2,000 figure deserves scrutiny. That is the inference cost of running a model that already exists. Training Astra required billions of dollars in compute, data, and research. The marginal cost of discovery is $2,000. The fixed cost of building the discoverer is several thousand times that. OpenAI confidentially filed its draft S-1 with the SEC on June 8 and is pursuing an IPO that could value the company near $1 trillion. The Astra announcement is both mathematics and marketing. The proofs are real. The timing is strategic.
The model is unreleased. No external researcher can reproduce the results by running Astra independently. But the Lean certificates can be verified by anyone with a laptop and the Lean 4 toolchain. The outputs are open. The system that produced them is closed. You can check the answer without seeing the work.
The Question
Mathematics is the only field where the work product can be mechanically verified to be correct. A diagnosis needs a doctor. A legal brief needs a lawyer. Generated code needs a review. A Lean proof needs a compiler. The certificate either type-checks or it does not. All ten type-check.
The Leiden Declaration concerns process. The proofs are not in dispute. The argument is about everything else. Whether discovering results this way, announcing them this way, and crediting them this way threatens the institutions that mathematics has used to govern itself for centuries.
Those institutions were built to answer one question: is the proof correct? Lean answers it in seconds. What the declaration defends is the right to ask a different question. Whether the discovery counts. Whether the method is legitimate. Whether $2,000 of computation should carry the same weight as a career spent learning to think about non-sofic groups. The proofs compile. The question that remains is the one no compiler can answer.