OpenAI has unveiled “Astra,” an as-yet-unreleased AI model said to have solved ten problems in mathematics and theoretical computer science that had been open for at least a decade – each backed by a machine-checkable formal proof.
Proofs anyone can verify
For the ten results, OpenAI published a 249-page manuscript plus formal proof certificates in the Lean 4 proof assistant – freely on GitHub under an Apache 2.0 license. The number of open proof gaps (the “sorry” count) is zero: every step is fully verified. Anyone can run the proofs against the published repository, so correctness no longer hinges on slow peer review.
What Astra solved
The results include an explicit construction of a “non-sofic” group – a question open since Mikhail Gromov defined soficity in 1999 – the disproof of Connes’ rigidity conjecture, a proof of Ehrhart’s volume conjecture and the resolution of three problems from Paul Erdős’s catalog, including problem 183 on multicolor Ramsey numbers.
Context
Importantly, none of the ten results has yet gone through regular peer review – the formal Lean verification stands in for it here. And the model itself is not yet publicly available. Still, the step is seen as a notable sign of how AI could seriously contribute at the research frontier.
