On August 1 OpenAI published a 249-page manuscript titled “Ten advances in mathematics and theoretical computer science,” reporting that an internal version of a model it calls Astra produced new results on ten problems where mathematicians had made no real progress for at least a decade, and in most cases far longer. Alongside the manuscript it published machine-checkable Lean 4 certificates for the results on GitHub under an Apache 2.0 license, with no unproven placeholders left in the files.
The ten results are the headline. The certificates are the news, and they change what kind of claim this is.
The Ten
The problems span pure mathematics and theoretical computer science:
| Area | Result |
|---|---|
| High-dimensional sphere packing | New upper bounds on density, down to the Cohn–Elkies threshold |
| Coding theory | Improved bounds for binary and spherical codes |
| Group theory | First explicit construction of a non-sofic group |
| Von Neumann algebras | Disproof of Connes’s rigidity conjecture |
| Arithmetic circuit complexity | New lower bounds for computing the permanent |
| Quantum complexity | Parallel repetition theorem for two-player entangled games |
| Lattice cryptography | Hardness of approximation for the closest vector problem |
| Convex geometry | Proof of Ehrhart’s volume conjecture |
| Ramsey theory | Multicolour Ramsey numbers, Erdős problem 183 |
| Extremal graph theory | Erdős problems 146 and 180 |
Two are worth understanding even if you never touch this material. The non-sofic group construction resolves a question Mikhail Gromov opened in 1999: soficity is a property that a great many theorems quietly assume, and for 27 years nobody could produce a group lacking it or prove that none existed. Astra produced one explicitly.
The sphere-packing result matters for a different reason. The best general upper bound on packing density in high dimensions came from the Kabatiansky–Levenshtein method in 1978. Improving that exponent is the first movement on a 48-year-old ceiling, and it lands in territory with direct bearing on lattice cryptography, which is the same neighborhood as the closest-vector-problem result on the list.
Why the Lean Certificates Change the Argument
Every prior AI-solves-mathematics announcement has asked the reader to trust the lab. You got a claim, a press release, and a wait for specialists to work through a manuscript. This one ships proofs a compiler can verify.
Lean is a proof assistant. It checks each logical step against strict rules and refuses to accept a gap. The files OpenAI published contain no sorry statements, Lean’s keyword for an admitted step you promise to fill in later, which means nothing is being taken on faith inside the formalization. Anyone with the Lean compiler and a laptop can confirm the proofs are valid without trusting OpenAI, its model, or its motives.
That is a genuinely different epistemic situation, and a rare one in this industry. Last month we were writing about OpenAI models trained against a leaked evaluation set, where the entire problem was that nobody outside the lab could check the claim. Formal verification removes that class of doubt entirely, because the proof is either valid or the compiler rejects it.
What the Certificates Do Not Cover
The verification is airtight about exactly one thing: these proofs are correct. It says nothing about how they were produced, and most of the interesting claims are about production.
OpenAI chose which results to publish. Ten successes tell you nothing about the denominator, and a model that attempts a thousand open problems and solves ten is a different artifact from one that attempts twelve. The reported compute cost of roughly $2,000 at Sol API rates covers the successful runs, not the search that found them, which makes it a striking number and an incomplete one. OpenAI staff assisted with formalization and manuscript preparation, so “the model did it” is doing compressed work in the summary. And nobody outside OpenAI can reproduce any of it, because Astra is unreleased.
So the honest statement is narrower than the headline. Astra produced ten correct proofs of hard open problems, verified beyond dispute. Whether it can do that reliably, at what hit rate, and how much human steering it needs are open questions that the Lean files were never going to answer.
There is also a presentational sleight worth noting: OpenAI announced its next major model family inside a mathematics paper. Astra got named, dated by implication, and positioned as a research instrument rather than a product, without a launch event or a benchmark table anyone could contest. It is an effective way to introduce a model, and it is a choice about framing rather than an accident.
The Leiden Problem
The timing is pointed. In June, an international group of mathematicians published the Leiden Declaration on Artificial Intelligence and Mathematics, which grew out of a 2025 workshop at Leiden University’s Lorentz Center. It gathered 130 signatures on its first day and passed a thousand within 24 hours, picked up Fields Medalist Peter Scholze, and was endorsed by the International Mathematical Union.
The declaration does not ask for a ban. It asks for disclosure of AI use, attribution when proprietary models are involved, and the preservation of rigorous review, and it warns specifically about companies announcing results by press release rather than through peer review. Two months later, OpenAI announced ten results by publishing a manuscript and a GitHub repository.
The uncomfortable part for the declaration’s position is that formal verification answers its strongest objection. If the worry is that AI proofs are hard to check independently, a Lean certificate with no admitted steps is a better answer than peer review, not a worse one, and it is available immediately rather than in eighteen months. The worries the certificates do not answer are the ones about attribution, about what happens to the training of new mathematicians, and about a discipline’s evidentiary standards being set by a company’s publication schedule. Those are real, and they are not technical problems with technical fixes.
Reaction from mathematicians has been warm on the substance. Thomas Bloom, who maintains the Erdős problems catalogue, called the results big news. On Astra’s earlier disproof of the Erdős unit-distance conjecture announced in May, Tim Gowers said that had a human submitted the paper to the Annals of Mathematics and he had been asked for a quick opinion, he would have recommended acceptance without hesitation. That endorsement was about the May result rather than these ten, and a team of nine mathematicians including Gowers and Noga Alon later published a companion paper rendering that proof in a form humans could follow more easily. The companion paper is the detail worth keeping: a machine-checkable proof establishes truth, and a separate human effort was still needed to establish understanding.
What This Actually Implies
The cheap conclusion is that AI is doing mathematics now. The more useful one is about where verification exists.
Astra’s results landed in fields where correctness can be mechanically confirmed. That is not a coincidence, and it generalizes: the domains that will absorb this capability fastest are the ones that already have verification infrastructure, meaning formal methods, chip design, cryptography, theorem proving, and parts of software engineering where a test suite or a type system can adjudicate. In those areas the cost of generating a candidate answer is collapsing while the cost of checking one stays flat, which shifts the bottleneck decisively toward checking.
Fields without that infrastructure get very little from this announcement, and arguably get a new problem. A model that produces plausible, well-argued, unverifiable output at scale is a burden on any discipline that reviews by reading, which is most of them. It is worth setting this against the AI-for-science tooling Anthropic shipped in June, aimed at wet-lab disciplines where no compiler will ever adjudicate the result. Mathematics happens to be the field best equipped to absorb this, and it is not obvious what the equivalent looks like in biology.
For anyone building with these models, the transferable lesson is unglamorous and immediate. The leverage is not in the generation step, which is getting cheap for everyone at once. It is in owning a way to tell whether the output is right. If you cannot check the work automatically, a more capable model mostly increases the volume of things you have to check by hand.
Sources
- Ten advances in mathematics and theoretical computer science — OpenAI
- OpenAI says its next model, Astra, has solved ten open problems in mathematics — The Next Web
- OpenAI’s Astra Solved Decades-Old Math Problems For $2,000 — Forbes
- OpenAI Astra’s 10 Math Proofs Explained — ExplainX
- Leiden Declaration on Artificial Intelligence and Mathematics — Wikipedia
- Leiden Declaration warns AI is challenging the core values of mathematics — Leiden University
- Why the Legendary Erdős Problems Are Falling to AI — Quanta Magazine