OpenAI releases ten Astra math proofs with Lean certificates

OpenAI has published ten proofs of previously open problems in mathematics and theoretical computer science, produced by an internal version of a model it is calling Astra. The list is not incremental sharpening of known results, it is a set of long-standing questions: a claimed counterexample to Connes's rigidity conjecture on group von Neumann algebras, a construction establishing that non-sofic groups exist, improved asymptotic upper bounds for high-dimensional sphere packing down to the Cohn–Elkies threshold, exponentially stronger bounds for binary and spherical codes, an n⁴/log n formula lower bound for the permanent, and a superexponential lower bound for multicolor Ramsey numbers resolving Erdős problem 183.

The part that makes this different from the usual AI-does-math press cycle is the Lean 4 formalization. Every one of the ten results ships with a machine-checkable certificate on OpenAI's GitHub repository, alongside a walkthrough of the model's reasoning. A Lean-checked argument is not the same as a peer-reviewed one, the human community still has to agree the formalized statement is the statement they care about, but it does close the loop on the most common failure mode of AI proof announcements, which is a plausible-looking chain that quietly hand-waves a step.

On cost, OpenAI's claim is that the tokens used to generate all ten solutions would have run about $2,000 at Sol's API rates, reports The Decoder, which also describes Astra as a "next major model family" built to coordinate multiple agents on long-running problems. The framing from OpenAI researcher Sebastien Bubeck, on X, is that these ten are illustrative, not exhaustive, of what the model has produced.

Take the specifics as reported, not settled. Astra is an internal model, external mathematicians have not had time to work through the arguments in the depth these conjectures usually attract, and the article does not spell out how much human problem-shaping preceded each run, which reviewers will have opinions on, or when the model becomes externally testable. Retractions on any single one of the ten would land loudly.

If even a majority survive scrutiny, the interesting shift is not a leaderboard win. It is that the cost of attacking a decade-old open problem starts to look like a cloud bill, and the pipeline that produces the attack outputs something a formal-methods tool can check. That changes who gets to try, and how fast.