OpenAI's Astra solves 10 long-open math problems and publishes the proofs
# Astra published proofs, not benchmarks
OpenAI released ten machine-checkable Lean 4 proofs on Friday, generated by an unreleased model called Astra. Each proof addresses a decade-old open problem in mathematics or theoretical computer science, including a construction that establishes the existence of non-sofic groups and new sphere-packing bounds down to the Cohn-Elkies threshold. The Lean repository reports a "sorry" count of zero, which means no step in any proof has been left unproven. Compute cost across all ten: about $2,000 at Sol API rates.
That last number is the one to sit with.
We are used to model announcements that trade in benchmarks. MMLU, GPQA, SWE-Bench, saturating this or that leaderboard. Astra debuted with something else: ten problems that were, on Thursday, unsolved, and on Friday, formally verified. Thomas Bloom, who curates the erdosproblems.com database, said the ten results are "big news." Timothy Gowers said he would recommend one of the proofs for the Annals of Mathematics without hesitation.
I have three things to say about that, as someone who ships AI products, not as a mathematician.
**One: the eval question just got easier and harder at the same time.**
Easier because Lean is not a leaderboard. It is a proof assistant. A proof either type-checks or it does not. There is no test-set contamination story to tell about a Lean certificate, no "we trained on the answers" retort. If OpenAI wanted to cheat this, they would have to smuggle a wrong proof past Lean's type checker, which is not the kind of thing that happens by accident.
Harder because most product teams cannot run this kind of eval on their own domain. Formal verification exists for math and a handful of software domains. For the domains I care about, health decision support, legal reasoning, contract review, agentic commerce, we do not have a Lean equivalent. The lesson to take from Astra is not "run more benchmarks." It is: find the strongest verifier your domain admits, and pipe your model's outputs through it before humans read them. A boring rules engine, a compiler, a linter, a database check, a policy engine. Anything that will type-check the model's work.
**Two: the cost line is where the story lives for anyone shipping.**
Two thousand dollars to solve ten open problems in mathematics. Take a moment with that. The number will be higher for you and me — the Sol rate is a wholesale rate, and Astra's per-token cost inside OpenAI is different from the rate the API will bear when the model ships. But even if the delivered price is 10x higher, the frontier for how much compute a hard reasoning task costs has moved. If you are still budgeting AI features on the assumption that a hard task costs tens of thousands of dollars in inference, redo the math.
The corollary: research teams inside companies just got interesting again. When the marginal cost of exploring a hypothesis with a frontier model drops by an order of magnitude, you can afford to fund questions you previously killed at the intake stage. Not "let the AI write the paper." Let the AI check the shape of an idea before you spend a person-month on it.
**Three: the release format is the message.**
OpenAI did not lead with a benchmark. They led with results plus verification. Paper, formal proofs, GitHub repo, Apache 2.0, sorry count zero. A working researcher can clone the repo, run Lean, and check the work by lunch. This is the release format I want from every lab going forward, translated to its domain. If you claim your model can do vulnerability research, ship the CVEs it filed. If you claim it can reconcile spreadsheets, ship the reconciliations plus the audit trail. Verifiable output is the new benchmark score, and the labs that lean into it will out-compete the labs still shipping evals nobody can reproduce.
Two counters I would take seriously if you brought them to me.
First, ten problems is a small n. It is. But "10 for $2,000" is a claim about the shape of the frontier, not the total volume. The interesting version of the eval is a follow-up manuscript in six months that says "we tried Astra on 200 open problems, it landed 40, and here is the distribution of what it got right." That paper will tell us whether Astra is a math oracle or a lucky reasoner with good taste in problems.
Second, the model is unreleased, so the results are unreproducible outside OpenAI. Fair. Until the model ships, treat the announcement as a capability signal, not a product input. What you can do today: read the paper, run one of the Lean proofs yourself, and form your own view on whether the arguments are the kind of thing you would sign off on if a human researcher brought them to you.
The narrower thing I am going to do this week: audit the verifiers in the two projects on my desk that make claims about correctness. If I am asking a model to produce output that a human then has to accept or reject, I want a Lean-equivalent in the loop. Not perfect. Legible.
If you have a domain where "verifier" is doing real work in your stack, reply and tell me what you use. I am collecting patterns.