On Friday into Saturday, OpenAI published something unusual: ten claimed results on long-open problems in mathematics and theoretical computer science, from geometry and coding theory to group theory and complexity — and, attached to each, a machine-checkable proof certificate. The flagship is a construction of an infinite, finitely presented non-sofic group, settling a question the mathematician Mikhail Gromov raised in 1999. It's a real step, and it needs a careful read, because the interesting part is not the headline. It's the fine print.

Who — or what — did the maths

OpenAI's claim is specific, and worth stating precisely because both the hype and the backlash tend to flatten it. The company says the mathematical arguments were generated by an internal model, while its own researchers worked with that model to turn the arguments into manuscripts, formalise the proofs, and — in OpenAI's words — take responsibility for their correctness.

So this is neither "an AI wrote a paper unaided" nor "a human used AI as autocomplete." It is the model producing the load-bearing mathematical ideas, with people doing the write-up and verification around it. OpenAI's Sébastien Bubeck put the strong version on X: the results were, he wrote, "proved by Astra, our next major model."

That name is itself a small tell. "Astra" is how OpenAI is marketing what it calls a new major model class, and it has not decided whether the thing ships as GPT-6 or as a point release in the GPT-5 line. In other words, the system that did this is not a product you can use. It's an internal version, shown off through its results.

The new part: it hands you the proof

The most substantive thing here isn't any single theorem — it's the format. Each of the ten results ships with a Lean certificate: a formal, machine-checkable version of the proof that a computer can verify line by line, published in an open repository (openai/ten-proofs) alongside chain-of-thought walkthroughs.

This matters because it inverts the usual problem with AI maths claims. Normally the announcement arrives first and the checking takes months. Here the checking tool arrives with the announcement: a Lean proof either compiles against the theorem statement or it doesn't. That's a real transparency step, and a rare one — it lets outsiders start verifying immediately rather than taking a lab's word.

The caveat, which skeptical mathematicians raised within hours, is that a formal certificate is only as trustworthy as its theorem statement and its soundness. A model optimising to produce compiling Lean code can, in principle, find shortcuts that satisfy the checker without proving what a reader thinks it proves — so the community's job is to confirm each certificate proves the intended statement, with an honest count of any axioms leaned on. A certificate that compiles is not the same as a result the community has checked — and that review has only just begun.

Why "claimed" is the operative word

Set the transparency step against what has not happened, and the honest label falls out. These results are self-published — a report plus a GitHub repo, not an arXiv paper, and not peer-reviewed. By OpenAI's own account, it judged only "at least five" of the ten as likely correct at release. And one of the ten has already been walked back: after outside analysis, OpenAI revised its assessment of the binary- and spherical-codes result. A set that loses one member to community scrutiny in its first days is a set to describe as claimed, not confirmed.

There's a second flattening to avoid, on the maths itself. Several of the ten are improved bounds rather than resolved conjectures — tighter limits on sphere-packing density, stronger bounds for error-correcting codes, sharper complexity estimates. Those are real contributions, but they are not the same act as constructing the non-sofic group or disproving Connes's rigidity conjecture, and a headline that says an AI "solved" ten open problems overstates the ones that are bound improvements.

The number nobody can check yet

OpenAI has leaned on the cost angle: its president Greg Brockman said the tokens needed to find all ten solutions would cost roughly $2,000 at the model's API rates — about $200 a problem. Treat that figure the way you'd treat any denominator-free statistic. As commenters on Hacker News noted immediately, it says nothing about how many attempts went into each success. Ten polished results selected and published tells you nothing about how many problems were tried and quietly dropped — which is exactly the information that would let you judge whether this is cheap genius or expensive fishing.

Independent reaction, so far, is thin rather than triumphant. The Manchester mathematician Thomas Bloom called it "big news" — while adding, honestly, that it's "not really my area." That is roughly where the verifiable outside commentary sits today: interested, not yet vindicating.

What it actually shows

Strip the naming and the cost framing away and something real remains. A frontier model produced mathematical arguments on hard, open problems, and — this is the part worth crediting — OpenAI shipped the results in a form built to be checked rather than merely believed. If the Lean certificates hold up under scrutiny, the non-sofic-group construction alone is a serious result, whoever, or whatever, found it.

But "if they hold up" is doing real work in that sentence, and the way to honour a proof you can check is to check it, not to announce it as settled. The most telling detail in the whole release is the one OpenAI supplied itself: one of the ten is already not what it first appeared to be. That's not a reason to dismiss the other nine. It's the reason to call all of them claims until the certificates — the good idea here — have done their job.