A multi-category news and explainer hub for timely stories, practical guides, and deep dives.
OpenAI says an unreleased model solved ten decade-old open problems. What makes this different from the company's last maths claim is not the results — it's a folder of files anyone can compile
On 1 August 2026, OpenAI announced that an internal, unreleased version of a model family it calls Astra had produced new results for ten problems in mathematics and theoretical computer science that had been open for at least a decade.
That sentence alone should not convince you of anything. OpenAI made a structurally similar claim ten months earlier and it fell apart within days.
What makes August different is not the announcement. It is what came attached to it: a 249-page manuscript collection, model-written walkthroughs of the reasoning, and a public GitHub repository of Lean 4 proof certificates released under an Apache 2.0 licence. As SiliconANGLE reported, the repository reports a sorry count of zero — sorry being the Lean keyword that marks a step the author has left unproven. Zero means no gaps were papered over.
You do not have to take OpenAI's word for any of this. You can download the files and compile them.
Per SiliconANGLE's breakdown, the headline result is an explicit construction of a non-sofic group. Soficity was introduced by Mikhail Gromov in 1999; loosely, a sofic group is one whose structure can be approximated by shuffling a finite deck. Every group anyone had ever examined turned out to be sofic, and nobody could prove they all were. Astra built the exception.
The model also disproved Connes's rigidity conjecture, posed in 1980, by constructing infinitely many non-isomorphic groups with property (T) that share the same von Neumann algebra — meaning the algebraic object that was supposed to act as a unique fingerprint does not, in fact, pin down the group it came from. It proved Ehrhart's volume conjecture, and it resolved three problems from Paul Erdős's catalogue, including problem 183 on multicolour Ramsey numbers.
The rest of the list spans high-dimensional sphere packing, binary and spherical codes, arithmetic circuit complexity, quantum parallel repetition, and the hardness of the closest vector problem — the last of which bears directly on lattice-based cryptography.
Two things are worth noting immediately. First, these are genuine open problems, not benchmark questions with hidden answers. Second, and equally important: none of the Clay Mathematics Institute's seven Millennium Prize Problems fell. Tech Times reported that OpenAI research scientist Noam Brown was candid about exactly that limit. The ten problems Astra solved were ones where enough existing theory gave it room to manoeuvre. Whether the same approach touches the hardest known problems is an open question, and OpenAI is not claiming it does.
Here is the part that matters more than any individual theorem.
Ordinarily, a claimed proof of a famous problem enters peer review. Human referees spend months working through the logic. The field waits. As Forbes put it, the Lean certificate collapses that timeline to the length of a download — verification and publication arrived on the same day.
Lean is a proof assistant. Its kernel returns a binary verdict: the proof compiles, or it does not. There is no room for a persuasive-sounding argument to slip through, and no requirement that you trust the entity that produced it. That property is why this announcement reads differently from a benchmark score.
The contrast with the previous approach is sharp. Tech Times notes that when OpenAI published an AI-generated disproof of the Erdős unit-distance conjecture in May 2026, validating it required nine external mathematicians to read and co-sign the argument. That is real validation, but it is social — it depends on qualified people being available and willing, and it cannot be reproduced by anyone else on demand. A Lean certificate can be re-run by anybody with a compiler.
This is where most of the coverage stops, and where it should not.
A successful Lean build confirms that the proof is valid for the theorem as formally stated inside Lean. It does not confirm that the formal statement faithfully captures the open problem as the mathematical community understood it. Translating an informal conjecture into a formal statement is itself a judgement call, and a subtly weakened statement can compile perfectly.
So the work has moved rather than disappeared. A mathematician still has to read each formal statement and confirm it says what the problem asks. And a mathematician still has to judge whether the result matters — Lean has no opinion about significance.
None of the ten has been through peer review.
There is also a difference between the May and August announcements that deserves to stay visible. As explainx.ai points out, the May unit-distance announcement explicitly described checks by outside mathematicians. The August release does not make the same broad external-review claim for the new set. That does not make the new results false. It means the validation status of the May result should not be silently transferred onto ten different August manuscripts.
In October 2025, OpenAI's then vice president of science, Kevin Weil, claimed that GPT-5 had solved ten previously unsolved Erdős problems. Thomas Bloom, who maintains the Erdős problems database, called it a "dramatic misrepresentation," per SiliconANGLE's account. The model had not solved anything — it had located existing papers in the literature that Bloom himself was unaware of. Weil deleted the post. Google DeepMind chief executive Demis Hassabis called the episode embarrassing.
That history is the single best reason to read the August claim carefully. It is also the reason the Lean files are the story. The failure mode in October 2025 — a retrieval result dressed as a discovery — is exactly the failure mode a machine-checkable certificate is designed to make impossible to sustain.
Bloom's own reaction to the Astra results was positive: SiliconANGLE reports he called them big news and rated them ahead of the unit-distance counterexample he had helped verify.
An honest reading concedes all three.
The problem set may have been selected. OpenAI chose which results to publish. We are seeing the wins.
The $2,000 figure is a cost of publication, not a cost of discovery. OpenAI put the token cost for all ten solutions at roughly $2,000 at GPT-5.6 Sol API rates. But as Forbes notes, that number covers the successful runs, not every attempt the model made. No walkthroughs exist for the problems Astra failed. We are reading the search behaviour of the winners only.
Humans were in the loop. Outside researchers have observed that OpenAI staff helped prepare the manuscripts and formalise the arguments. OpenAI's position is that the mathematical arguments themselves came from Astra, and its announcement says attribution should honestly reflect how results were produced.
To which add a fourth, which is not an objection so much as a structural fact: Astra itself is not available. The certificates are public. The model is not. Nobody outside OpenAI can pose it a new problem.
The timing is uncomfortable. On 2 June 2026, the International Mathematical Union endorsed the Leiden Declaration, which warns that AI companies are using published research without consent, bypassing peer review, and threatening the integrity of proof and attribution. Tech Times reports the declaration names five risks — unreliable results, missing citations, dependence on closed commercial systems, exaggerated claims, and loss of scientific independence — and has drawn signatories including Fields Medallists Terence Tao and Peter Scholze.
Anchoring the release in machine-verifiable certificates answers two of those five directly: unreliable results and exaggerated claims. It answers the "dependence on closed commercial systems" risk not at all, and arguably makes it worse. The best mathematical tool in the world being a private system you cannot query is precisely the concern.
Tao's own framing is worth sitting with. In a recent lecture he warns of "proof indigestion" — generation has become cheap while verification has not, and not every proof produced is a proof worth reading. He has also argued that mathematics is not uniform: a system may be strong at one part of the work and absent from another. Solving stated problems and building new theory are different capabilities, and nothing in the Astra release demonstrates the second.