OpenAI Astra: what the ten Lean proofs actually prove

OpenAI put ten proofs on GitHub on 1 August and didn't ship a model. That's the shape of this one: an internal version of Astra, its next model family, produced new results on ten problems that had been open for at least a decade, and what you can actually download tonight is a 249 page manuscript plus a repository of Lean files. We cloned it. The model stays private, the proofs don't, and every result carries a machine-checkable certificate, so correctness is a question you can settle on your own laptop instead of trusting a launch post. Correctness is the easy half. Whether any of it matters mathematically is a separate question, and so is what that $2,000 figure is really counting.

What actually shipped

Three artefacts, none of them a model. A 249 page manuscript. A set of narrated walkthroughs of the model’s reasoning. And a Lean repository.

The results came from what OpenAI calls “an internal version of Astra, our next major model.” Astra is the family that would sit above the Sol, Terra and Luna tiers we went through when GPT-5.6 went public. Nobody outside the lab has an API key for it, which is worth holding onto while you read the rest.

Image: OpenAI

The ten cover sphere-packing upper bounds down to the Cohn-Elkies threshold, exponentially improved bounds for binary and spherical codes, a construction establishing that non-sofic groups exist, a disproof of Connes’s rigidity conjecture, an arithmetic-formula lower bound of order n^4/log n for the permanent, an exponential parallel repetition theorem for two-player quantum games, polynomial-factor hardness of approximation for the closest vector problem, the sharp Ehrhart volume bound in every dimension, a superexponential lower bound for multicolor triangle Ramsey numbers, and counterexamples that settle Erdős problems 146 and 180. OpenAI’s framing: each had “seen no progress on the main result for at least a decade, and in most cases much longer.”

Then the number everyone quoted. From the announcement: “The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.”

The part you can check tonight

Here’s what makes this release different from the usual lab claim. Go and get it:

The repository is openai/ten-proofs, Apache 2.0, created on 1 August. Ten .lean files plus an All.lean that pulls them together. The toolchain is pinned to leanprover/lean4:v4.32.0 against mathlib, so the build is reproducible rather than a screenshot of one.

The file we’d actually open first is formalization.yaml. It reports sorry_count: 0 and sorry_in_definitions: 0, so no result is propped up by an admitted gap. Each theorem also lists its axioms, and for all ten they are propext, Classical.choice and Quot.sound. That trio is what ordinary Lean mathematics runs on. Nothing exotic was quietly added as an assumption, which is the classic way a formalized claim goes bad.

Two other lines in that file got less attention than they deserve. The automation block records the method as an agent, the framework as Codex, and the wall time as one week. And the review status reads agent-reviewed.

Not human-reviewed. Their own metadata says so.

What a compiler can’t tell you

Lean will confirm that a formal statement follows from the axioms. It will not tell you the formal statement is the one the field cares about. Read a theorem statement in a paper and you are reading English; read one in Lean and you are reading a definition chain that a specialist has to walk to be sure the quantifiers land where they should. For something like Connes’s rigidity conjecture, that walk is not a weekend.

So the honest position on day two is that the proofs are very likely correct and their importance is unestablished. Those aren’t in tension.

The $2,000 has the same shape of problem, which Noam Brown said out loud himself:

And yes we did try other major problems without success. Sadly no Millennium Prize problems (yet). But also, we didn’t spend a lot on each problem. It’s possible to push test-time compute much further.

Noam Brown (@polynoamial), 1 August 2026, on X.

Read that against the headline. The $2,000 counts winning runs. No attempt count, no failure rate, nothing to divide by. It’s a cost-per-success figure wearing a cost-per-problem costume, and I don’t think that’s deliberate spin so much as the natural thing to publish when the failures produced nothing to show.

Credit where it’s due on attribution, though. OpenAI wrote that “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,” and stated that humans prepared the manuscripts and the formalizations while the arguments came from the model. That’s a cleaner disclosure than the Fable 5 Jacobian conjecture counterexample got, and a lot cleaner than May’s Erdős unit-distance episode, which is what prompted the Leiden declaration OpenAI now cites by name.

The line that’s going to get misread

One of the ten is polynomial-factor hardness of approximation for the closest vector problem, which OpenAI describes as “a foundational lattice question related to post-quantum cryptography.”

If that sentence made you open your migration tracker, close it. It’s a hardness result. It says approximating CVP within a polynomial factor is NP-hard, which pushes in the same direction the lattice assumptions already lean. Nothing here weakens ML-KEM or ML-DSA, and our notes on post-quantum TLS stand unchanged. Honestly, I’d bet this ends up the most misquoted line in the release.

As for when you can point Astra at your own backlog: not yet, and possibly not purely on OpenAI’s schedule. Sam Altman spent the end of July demonstrating it to senators and administration officials in Washington, and multiple outlets report a new federal framework requiring pre-release review of frontier models, with Astra expected to be the first through it. We haven’t seen the text of that framework, so treat the timing as reported rather than settled.

What we’d do with the release right now is unglamorous. Clone the repo, build one module, and see how long mathlib takes on your machine. Whatever else this week produced, a lab shipping a claim you can falsify with a compiler is a better default than the alternative.

Sources

OpenAI, Ten advances in mathematics and theoretical computer science, 1 August 2026, for the results list, the $2,000 claim and the attribution statement. The Lean files, toolchain pin, axiom lists and metadata come from the openai/ten-proofs repository, read directly. Noam Brown’s remarks are quoted from his post on X of 1 August 2026. Cross-checked against The Decoder and Implicator, which also cover the Washington demonstrations and the pre-release review framework. Announcement artwork is OpenAI’s own, reproduced as a credited citation.

Frequently asked questions