On 2 August 2026, OpenAI announced its next major model by publishing a document titled Ten Advances in Mathematics and Theoretical Computer Science. The model is called Astra, and the ten results were the announcement.
The list is unusually broad: high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes's rigidity conjecture, arithmetic circuit complexity, quantum parallel repetition, the closest vector problem, Ehrhart's volume conjecture, multicolour Ramsey numbers and extremal number conjectures. The common thread given was that none had seen progress on its central result for at least ten years, and most for considerably longer.
Sorry count zero
The proofs were released as Lean 4 files with a sorry count of zero. In Lean, sorry is the keyword that lets you leave a gap and carry on, so a file containing none is a proof with nothing taken on trust. The compiler checks it against the axioms in seconds, and either accepts it or does not.
That is the detail that separates this kind of announcement from a claim about a benchmark. You do not have to believe OpenAI about whether the proofs are correct, and you do not have to wait for a referee. You can download the files and run Lean. What remains open to argument is whether the formal statements are faithful to the problems people meant, which is a real question but a much smaller one.
The reported cost was about $2,000 in tokens for all ten solutions. Whether that figure is comparable to anything is unclear, but it is a long way from the usual framing of mathematical research as a scarce and expensive activity.
The Ramsey entry
Multicolour Ramsey numbers are a good illustration of why this family of problems is hard. The two-colour case asks for the smallest group in which you are guaranteed either s mutual friends or t mutual strangers. R(3,3) is 6. R(4,4) is 18. R(5,5) has been open for seventy years and is known only to sit between 43 and 46.
The reason is not lack of effort. The Ramsey bounds calculator makes it concrete: the Erdős-Szekeres bound puts R(5,5) at no more than 70 vertices, and checking every two-colouring of a 70-vertex graph means about 10 to the power 727 cases. Even at the true answer of 46 or below, it is around 10 to the power 311. There are fewer than 10 to the power 82 atoms in the observable universe, so this is not a problem that waits for faster computers.
Multicolour versions are worse again. R(3,3,3) is 17 and almost nothing else is known exactly. Progress there is measured in bounds, not values.
How to read it
With the same care you would apply to any announcement from the organisation that built the thing. The phrase used was "solved or made significant progress on", which covers a range, and ten results across ten fields is a lot of surface area for a reader to check.
But the formal proofs are the answer to most of that. A company can characterise its own results generously; it cannot make Lean accept a proof that does not hold. The pattern is the same one in the AlphaProof Nexus work from three months earlier, and it is becoming the standard by which these claims are judged.