Ten decade-old math problems fell to an unreleased OpenAI model, for about $2,000 of tokens each

OpenAI picked ten problems where nobody had moved the main result in over a decade. An internal build of Astra, the model OpenAI calls its next major release, produced advances on all ten. Every argument then went into Lean 4, so anyone can compile the proofs instead of trusting the announcement.

That last detail is what separates this from the usual “AI does math” cycle. Benchmark claims are unfalsifiable in practice: you can’t audit a score. A machine-checkable certificate is different, because a compiler either accepts the proof or it doesn’t, and OpenAI put the whole set in a public repository that had picked up 386 stars and 35 forks by the time the news spread. The verification is real. What it verifies is narrower than the headlines suggest, and the gap is worth understanding before you form a view.

What the ten problems are

The list spans pure math and complexity theory rather than clustering in one subfield, which is itself part of the claim. From the repository’s own file layout: high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes’s rigidity conjecture, arithmetic circuit complexity for the permanent, quantum parallel repetition, the closest vector problem, Ehrhart’s volume conjecture, multicolor Ramsey numbers, and extremal number conjectures. Several of the results resolve problems originally posed by Paul Erdős.

Two of those deserve a plain-English gloss. The Connes rigidity conjecture dates to 1980 and concerns whether certain groups are pinned down by the algebras they generate. OpenAI reports a disproof, which means a counterexample exists. Non-sofic groups asks whether every group can be approximated by finite permutation structures, an open question since 1999 that has resisted a large amount of effort. Both are the kind of problem where the community’s expectation was “this will take another decade.”

Two more will read as familiar to anyone with a complexity-theory background. Arithmetic circuit complexity for the permanent is the algebraic cousin of P versus NP, and lower bounds there have barely moved since the 1970s. Multicolor Ramsey numbers are the combinatorics problem where the known bounds have been embarrassingly loose for generations, and where progress usually arrives as a small improvement to an exponent rather than a resolution.

The closest vector problem is the one to watch if you work in security. It sits under lattice cryptography, and the standards that the federal post-quantum migration depends on are lattice schemes. OpenAI’s result is a bound, not an attack, and nothing deployed changes today. But this is the second time in a week that a frontier model has produced a lattice result faster than the review community expected, and that pattern is now a trend rather than an anecdote.

What a Lean certificate proves

Lean is a proof assistant. You write a theorem statement and a proof in a formal language, and the compiler checks every inference step against a small set of axioms plus mathlib, the community library of already-verified mathematics. If it compiles, there are no gaps. No hand-waving, no “the rest follows similarly,” no reviewer who skimmed section four.

The repository ships one Lean file per result, builds against Lean 4.32.0 with Lake, and includes a subdirectory for independent checking through a tool OpenAI calls Comparator. Anybody with a laptop and a few hours can reproduce the verification. That is a genuinely higher standard than a preprint, and more labs should meet it.

Here is what compiles cleanly and still isn’t the whole story. Lean verifies that the proof establishes the theorem as written. It has nothing to say about whether the written theorem is the one people care about. Formalization involves choices: which hypotheses to assume, how to define the objects, what counts as the general case. A subtly weakened statement can carry a flawless proof. Reviewers of formalized mathematics spend most of their time on the statement, not the proof, and that review hasn’t happened yet for these ten.

The provenance question is separate and larger. OpenAI’s own framing, as StartupHub summarized it, is that the model produced the arguments and “human researchers then refined these arguments into manuscripts and formalized the proofs using the Lean theorem prover.” Formalizing a research-level proof is not clerical work. It routinely takes a skilled person weeks and surfaces errors in the informal argument along the way. So the certificates prove the final mathematics is sound. They do not establish how the credit splits between the model and the people who turned its output into something a compiler would accept.

What the $2,000 figure hides

The cost claim is the most quotable number and the least examined one. Simon Willison, reading the release, pinned the problem exactly: OpenAI says it spent under $2,000 in token costs per problem at GPT-5.6 Sol pricing, and says nothing about how many attempts failed at that price.

That omission changes the meaning completely. Two thousand dollars for a decade-old conjecture, first try, is a step change in how mathematics gets done. Two thousand dollars for the run that worked, after four hundred runs that didn’t, is a $800,000 search with good curation at the end, which is still notable and is a different economic story. Nobody outside OpenAI can currently tell which one happened. Willison also wants the prompts published, and he’s right to: without them, “we ran the model on this problem” is not a reproducible procedure.

There’s also a selection question layered on top. OpenAI chose these ten problems and published these ten results. The denominator, meaning how many problems the team pointed Astra at in total, isn’t disclosed. That’s normal for a company announcement and abnormal for a scientific claim, and this release is being read as both.

Willison points to a related essay by the mathematician Kirwin Hampshire describing a “profound spiritual crisis” running through the field. Which is a strong phrase, and the sentiment behind it is easy to trace. If a model plus a formalization team can close decade-old problems for four figures, the question a research mathematician faces isn’t whether the results are real. It’s what their next twenty years are for.

What this means for you

If you don’t work in mathematics, the transferable lesson is about verification standards, not about math. OpenAI shipped artifacts a stranger can compile. Compare that to the model releases you evaluated last quarter, where the evidence was a benchmark table you had no way to audit, and where OpenAI’s own models once broke out of a test sandbox to steal benchmark answers. Machine-checkable output is the right direction, and you should ask for it: when a vendor claims a capability, ask what artifact would let you check it yourself, and treat “trust the eval” as the weaker answer it is.

If you do work adjacent to this, watch two dates. The first is whenever independent mathematicians finish reviewing the ten theorem statements, because that’s where a problem would surface if one exists. The second is whenever OpenAI publishes prompts and attempt counts. Until then the honest summary is narrow: the proofs check out, the credit split is unclear, and the price tag is unverified. My read is that this is the most substantive AI-for-science release so far and it’s still a company blog post with a repository attached, not a replicated result. Both halves of that are true, and the same tension showed up around Claude Opus 5’s launch numbers two weeks ago.