OpenAI's next model has a name, Astra, and ten proofs a machine can check

Ten problems. Each had gone at least a decade without progress on the main result, and most of them very much longer than that. On 1 August OpenAI published all ten in a single 249-page manuscript, and said the arguments in it came from an internal version of Astra, the company’s next major model.

OpenAI calls Astra “our next major model”, the successor to the GPT-5.6 line. The version that did this work is internal, and nothing about it has been released.

The results span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. Several of them close questions that have been sitting in textbooks for a generation.

“This is the first improvement since 1978 to the general sphere-packing exponent.”

OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, chapter 1

The sphere-packing chapter carries the cleanest headline claim in the manuscript. Kabatianskii and Levenshtein set the general exponent at 0.59905576 in 1978, and everything since had improved only lower-order factors. The new exponent is ½ log₂(2π/e), or 0.6044. In the paper’s own words, “this is the first improvement since 1978 to the general sphere-packing exponent”. A matching lower bound comes with it, which says no Cohn–Elkies auxiliary function can ever do better.

The non-sofic construction is older still as a question. Gromov introduced the approximation property in 1999, Weiss named sofic groups and asked whether a non-sofic one exists in 2000, and the answer had been open for twenty-six years.

The certificate is the story

Announcements about machines doing research mathematics arrive regularly, and they are usually impossible for an outsider to evaluate. A 249-page manuscript in operator algebras can be assessed by perhaps a few dozen people on earth, and it takes them months.

What OpenAI shipped alongside it changes that arithmetic. The company published a repository of Lean 4 files, one per result, under Apache-2.0. A Lean file is not a description of a proof. It is the proof, written so a computer either accepts it or refuses it, with no room for a referee to be tired or generous.

The repository’s manifest is where to look. For all twelve theorem declarations covering the ten results, formalization.yaml records sorry_count: 0, meaning not one step is left as an unproved placeholder, and lists the axioms each one leans on:

sorry_count: 0
axioms: ["propext", "Classical.choice", "Quot.sound"]

Those three are the standard classical axioms that come with Lean’s core and mathlib. Nothing beyond them is assumed anywhere in the ten proofs. Anyone with elan installed can run lake exe cache get && lake build All and find out for themselves, on a laptop, this afternoon.

OpenAI went one better and included challenge configurations for Comparator, the proof judge built by the Lean FRO. Comparator checks three things in a sandbox: that the submitted proof proves the same statement as the challenge, that it uses only permitted axioms, and that the kernel accepts it. It can also run the check through the independent nanoda kernel rather than Lean’s own, so a sceptic does not have to trust the Lean kernel either.

That is a genuinely unusual thing for a lab to hand its critics.

The repository, as it stands. One file per result, and the manifest that records no gaps in any of them.

What the certificates do not settle

A Lean certificate proves that a theorem follows from the axioms. It says nothing about whether the theorem, as formalised, is the theorem the field cares about. Translating “Connes’s rigidity conjecture is false” into a Lean declaration is itself a mathematical act, and it is the step where a formalisation can be technically flawless and still miss.

OpenAI’s own manifest flags this. Under review, the file reads:

review:
  status: "agent-reviewed"

The formalisation was reviewed by an agent. The same automation block names the model as “Astra (OpenAI)”, the framework as Codex, and the wall time as one week.

The register of record has not moved either. The Erdős Problems database, the catalogue where these questions are tracked, still lists all three of the problems OpenAI says it resolved as open as of today, each carrying the standing note that no solution has been claimed in the comments. Problem 183 has a $250 prize on it, problem 146 has $500.

Read that for what it is. The database is maintained by hand, it says on every page that its status “reflects the current belief of the owner of this website”, and a paper published this morning is not going to be reflected in it by this afternoon. It is not a verdict.

Problem 183 on the afternoon of 1 August, with the maintainer’s own caveat underneath it. The page’s footer records it as last edited on 10 April 2026.

It is, though, an accurate picture of where independent verification stands on day one, which is that it has not happened. The certificates exist precisely so that it can happen faster than the usual months.

The disagreement about credit

Two months before any of this, on 2 June, the mathematical community published the Leiden Declaration on Artificial Intelligence and Mathematics. It carries the endorsement of the International Mathematical Union and, at the last count on its own site, 3,348 signatures, among them Peter Scholze, Terence Tao, Kevin Buzzard and Jeremy Avigad.

Its position on credit is not ambiguous. “Credit and responsibility continue to belong to humans within the mathematical community”, and should not be given to automated systems. Responsibility for the correctness of an argument “remains exclusively with the human authors”.

“Credit and responsibility continue to belong to humans within the mathematical community.”

The Leiden Declaration on Artificial Intelligence and Mathematics, 2 June 2026, endorsed by the International Mathematical Union

OpenAI links that declaration by name, says it has “deep respect and understanding for those concerned with its impact, including the signers”, and then takes the opposite view:

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.

It splits the declaration’s two halves and keeps one. Responsibility for correctness, OpenAI accepts. Authorship of the mathematics, it declines, on the grounds that taking it would be dishonest.

Both positions are arguable and both are held in good faith. They cannot both become the convention, and the question is now in front of the discipline in concrete form rather than as a thought experiment: a paper on the Cohn–Elkies bound with no human author, and a working proof to go with it.

Named mathematicians do appear in the manuscript, in the acknowledgments, thanked for comments. The Connes chapter credits Sorin Popa “for valuable comments on the historical context, the countability theorem, and the finite-to-one question”, and François Charles and Cyril Houdayer for careful readings. The non-sofic chapter thanks Henry Bradford, Michael Chapman, Alon Dogon and Francesco Fournier-Facio. That is the traditional role of the reader who improves a paper, and it is doing new work here: those are the humans in a document with no human authors.

The price

The figure travelling fastest is the cheapest thing in the story, and it deserves reading exactly as written. OpenAI says “the total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates”.

Three qualifications sit inside that sentence. It is the cost of the tokens that found the solutions, not of the research programme. It is priced at Sol rates, the current commercial tier, rather than at whatever an internal Astra would cost. And it excludes the week of agent wall time, the human work of turning the arguments into manuscripts, and the formalisation pass.

Even discounted for all three, it is a striking number to put next to twenty-six years of an open question.

The line in chapter four

The most interesting sentence in the manuscript is buried at the end of the Connes chapter, after the acknowledgments:

During the preparation of this manuscript, we learned of independent and concurrent work by Shuoxing Zhou also establishing a counterexample to Connes’s rigidity conjecture, developed in part with the assistance of GPT-5.6 Sol.

Connes’s conjecture grew out of his 1980 rigidity theorem, goes back to his Kingston proceedings article of 1982, and appears as Problem 1 in his 1994 monograph. It was disproved twice in the same season, by two groups, both working with a language model, neither aware of the other. Simultaneous discovery is an old story in mathematics. Simultaneous discovery on this schedule is not.

What is not known

Astra has no release date, no benchmark card, and no public availability. Nothing has been said about its size, its training, or how it differs from the GPT-5 line beyond the results it produced here.

No independent mathematician has yet published an assessment of the ten arguments, and no one outside OpenAI has reported building the Lean project end to end. The formalisations carry an agent review, not a human one.

The reasoning walkthroughs OpenAI released run to 62 pages across all ten problems, which is a narration of the model’s thinking rather than a log of it. How the arguments were actually found, and how many attempts failed on the way, is not in the record.

What is in the record is ten files, three axioms, and no gaps. That part anyone can check.