OpenAI says an unreleased version of its next major model produced solutions to ten mathematics problems that had gone unsolved for at least a decade. For every one, the company published a machine-checkable proof. It revealed the work on August 1, using it to name the model family Astra. OpenAI puts the total compute cost at roughly $2,000, at the company's API rates.
The results came as a 249-page manuscript covering group theory, high-dimensional geometry, coding theory, quantum complexity, lattice cryptography and combinatorics. The headline is the first explicit construction of a non-sofic group. A "sofic" group is one that can be closely approximated by finite systems of permutations, and until now no one knew whether any group could fail that test. The mathematician Mikhail Gromov introduced the idea of soficity in 1999. No one had built such an example in the 27 years since. Other results disprove the Connes rigidity conjecture and prove Ehrhart's volume conjecture — two long-open questions in algebra and geometry — and settle three problems from Paul Erdős's famous list.
Unlike some earlier OpenAI claims — one from 2025 was publicly disputed — these results can be independently checked. OpenAI wrote each argument in Lean, a proof-checking language, and posted the files to a public repository. Lean forces every logical step to be spelled out, then a small trusted program either accepts the whole proof or rejects it. The repository reports a "sorry" count of zero, meaning no step was left unproven. Anyone with the software can verify the results without trusting OpenAI or holding a mathematics PhD.
Among the first mathematicians to weigh in on the published Lean code was Thomas Bloom, a University of Manchester mathematician who runs the erdosproblems.com catalogue. He called the results "big news" on X and rated them more significant than a counterexample OpenAI published in May. He publicly picked apart an earlier, overstated OpenAI math claim in 2025, and he pushed back on the idea that the new work means AI is replacing mathematicians.
Beyond the checkable facts, the significance is still being weighed. Lean confirms that each proof holds together logically. It does not confirm that a problem was written down to mean what mathematicians actually intended, so human reviewers still matter. None of the results have gone through a refereed journal. And, as OpenAI researcher Noam Brown noted, none of the seven Millennium Prize Problems fell to Astra. The $2,000 run cracked hard problems, but not the hardest ones.
The timing is delicate: in June, mathematicians published the Leiden Declaration, endorsed by the International Mathematical Union, warning that AI labs are announcing results through press releases instead of peer review. Astra itself is not yet public, and OpenAI has not set a release date. For readers, the thing to watch is not the headline number. It is whether independent mathematicians, working from those public Lean files, confirm the proofs and fold them into the normal record. If they do, the cost of producing genuinely new mathematics may have just dropped in a way the field will have to reckon with.
