OpenAI's Astra Solved 10 Open Math Problems, With Lean Proofs

OpenAI announced Astra, its next major model, by publishing new results on ten long-open problems in math and theoretical CS. Every proof ships with a machine-checkable Lean 4 certificate.

··6 min read
aiopenairesearchreasoning
OpenAI's Astra Solved 10 Open Math Problems, With Lean Proofs
On this page

On August 1, 2026, OpenAI announced Astra, its next major model, by publishing results on ten long-open problems in mathematics and theoretical computer science. Every result ships with a machine-checkable Lean 4 certificate, the whole run cost roughly $2,000 in tokens at Sol tier rates (per Greg Brockman and Noam Brown), and none of the problems had seen progress on their main results in at least a decade. The model itself is unreleased. This post covers what was solved, how it was verified, and where the announcement lands.

TL;DR OpenAI published "Ten advances in mathematics and theoretical computer science" on August 1, 2026, announced on X by Sébastien Bubeck. The ten results span discrete geometry, coding theory, group theory, operator algebras, circuit complexity, quantum complexity, lattice cryptography, and extremal combinatorics. Headlines include the first explicit construction of a non-sofic group (open since Gromov 1999) and the first improvement to the Cohn-Elkies sphere-packing bound in 48 years. Every proof is formalized in Lean 4 and open-sourced on GitHub with zero sorry count. Astra is closed and internal, so no ChatGPT availability, no pricing, no model card. The verification is real. Peer review is not done yet.

The setup

OpenAI selected ten problems that shared one property: no progress on the main result for at least a decade, and much longer in most cases. The fields are deliberately diverse. Discrete geometry. Coding theory. Group theory. Operator algebras. Arithmetic circuit complexity. Quantum complexity. Lattice cryptography. Extremal combinatorics.

An internal version of Astra was given each problem and produced a construction, counterexample, or bound. The mathematical arguments were generated by the model. Humans prepared the arguments into manuscripts. The model itself then formalized each argument in Lean 4, and the certificates were pushed to openai/ten-proofs under Apache 2.0. Each result gets its own plainly named file: NonSoficGroup.lean, SpherePacking.lean, ConnesRigidity.lean, and so on. The repository's sorry count, Lean's way of marking any unfinished step, is zero.

Alongside the code, OpenAI published a 249-page manuscript of the arguments and 62 pages of narrated discovery notes showing how the model reached each solution.

The ten results

Six headline Astra results: sphere packing, non-sofic groups, Connes rigidity, permanent lower bounds, multicolor Ramsey, plus four more spanning codes, quantum, lattice, and Ehrhart volumes

The full list is technical. Five results are worth naming.

  • Non-sofic groups (NonSoficGroup.lean). An explicit construction of a group that is not sofic. Mikhail Gromov introduced soficity in 1999 as a weakening of amenability, and whether every group is sofic has been open ever since, 27 years. This is the headline.
  • Sphere packing (SpherePacking.lean). A new upper bound on sphere-packing density in high dimensions, the first improvement to the general Cohn-Elkies bound since 1978. A 48-year gap in a corner of geometry that produced a Fields Medal as recently as 2022.
  • Connes's rigidity conjecture, disproved (ConnesRigidity.lean). Astra constructed non-isomorphic groups with property (T) that share the same von Neumann algebra. Connes had conjectured the algebra determines the group up to isomorphism.
  • New circuit lower bounds for the permanent (Permanent.lean). A well-known frontier in arithmetic circuit complexity. OpenAI researcher Lijie Chen, on leave from UC Berkeley, singled this out publicly.
  • Multicolor Ramsey numbers (MulticolorTriangleRamsey.lean). A superexponential lower bound resolving Erdős problem 183, from Erdős's catalog of open problems.

The other five: QuantumParallelRepetition.lean (quantum complexity), GapCVP.lean (hardness of the closest vector problem, relevant to post-quantum cryptography), MetricCodes.lean (binary and spherical codes), EhrhartVolumeInequality.lean (lattice polytope volumes), and CompactnessAndDegeneracy.lean (a second problem from the Erdős catalog).

OpenAI's own framing is that each result "either resolved an open problem or made substantial progress on one," which is worth carrying forward from claim to claim.

Verification via Lean 4

Lean is a proof assistant with a small trusted kernel. You write your argument as code, the kernel checks it, and returns pass or fail. There is no room for a persuasive but subtly broken argument to sneak through. That is what makes formal verification useful here.

The Lean certificates take one specific thing off the table: whether the argument, once written, is correct. The kernel says yes or no. What Lean does not take off the table:

  • Whether the formal statement in Lean matches what the open problem is actually asking. A theorem that proves a variant of the question is still a valid Lean proof, but it does not resolve the original.
  • Whether the result is mathematically important. Compilation is not significance.
  • Whether the proof method generalizes or is a one-off.

Every one of those needs a mathematician to read the paper, not a machine to run the certificate. That is why "none has been through peer review" is a footnote worth taking seriously.

Astra vs AlphaEvolve

Astra versus AlphaEvolve compared across what each produces, how each is verified, whether the loop is disclosed, results, and cost signal

Both AlphaEvolve and Astra get proposed as evidence that models can now discover new mathematics. The two systems solve very different classes of problem.

  • Verification surface. AlphaEvolve evolves code and verifies it by running it against a user-supplied scoring function. Astra proves theorems and verifies them against Lean's kernel. Both are automatic. AlphaEvolve's surface is "does the code produce a better number." Astra's is "does the kernel accept the proof."
  • Loop shape. AlphaEvolve is public about its architecture: an evolutionary loop pairing Gemini Flash and Gemini Pro, with a program database that balances exploration and exploitation. Astra's loop is not disclosed. OpenAI shares the outputs and the reasoning walkthroughs, not the harness.
  • Scope of result. AlphaEvolve reported three production wins: matrix multiplication (rank-48 for 4x4 complex), 0.7% compute recovery in Borg, and 23% kernel speedup on Gemini training. Astra reports ten formal results across eight fields of pure math and TCS.
  • Cost. AlphaEvolve's costs are not published in unit form. Astra's ten solutions used tokens that would cost roughly $2,000 at Sol tier API rates.

Different tools, different problems, same underlying claim: an evaluation surface a model can iterate against is what makes autonomous discovery possible.

Cost and compute

The $2,000 number is the most-repeated line from the announcement, and worth reading carefully. It is the token bill at GPT-5.6 Sol tier rates ($5 per million input tokens, $30 per million output tokens as of July 2026) for the tokens used across all ten problems combined, not a per-problem average of anything meaningful. Noam Brown, one of the researchers on the test-time reasoning work behind Astra, added a caveat on X: "We didn't spend a lot on each problem. It's possible to push test-time compute much further."

The Millennium Prize problems, which offer $1 million each for solutions, were tried and not solved. Brown said so directly. That fact is as important as the ten that were. It sets the current frontier: hard, decade-plus-open problems with clean formal statements are inside reach for a system like Astra. Wide-open frontier conjectures are not, yet.

Worth noting: in May 2026, OpenAI shared a separate Astra-produced disproof of the Erdős unit-distance conjecture during evaluation. Add that to the tally and it is eleven, though OpenAI packaged ten as the official set.

Caveats

Three that matter, none of which are hidden.

  • Not peer-reviewed. OpenAI's mathematicians vetted the proofs. Independent mathematicians will need weeks to months to work through the 249-page manuscript. Some results may weaken on review, and some may hold.
  • Selection effect. Researchers have publicly asked whether problems were chosen partly because they were tractable for the model. Ten hard problems selected from a much larger set is a different claim than ten hard problems chosen at random.
  • Astra is unreleased. There is no model card, no API access, no pricing, no ChatGPT availability. What exists publicly is the announcement, the manuscript, the Lean certificates, and the discovery notes. The system that produced them is not available to check its work on new problems.

Why it matters

The correct response is neither instant dismissal nor instant acceptance.

The Lean certificates change the character of the announcement. Previous "AI solved a math problem" claims lived and died on human review of the argument. This one has already passed the kernel. That is a stronger baseline than the field is used to, and it makes the claim harder to dismiss on principle.

What is left to argue about is what has always been left to argue about: whether the formal statement matches the original question, whether the results generalize, whether the method is doing math or doing search over a very large space of Lean tactics until something compiles. Those arguments will take months, not tweets.

The other read is about capability. If test-time compute at Sol rates can produce ten formal results across eight fields for $2,000, the shape of the frontier changes. Not because the Millennium Prize problems fell (they did not), but because the class of "hard, formally stateable, decade-plus-open" problems just got a new tool. That tool has known limits and known caveats, and it is not in your ChatGPT yet.

Sources