OpenAI published ten new mathematical results on 1 August 2026, and said every one of them was produced by an unreleased internal version of a model it calls Astra. The problems span pure mathematics and theoretical computer science: how densely spheres can be packed in very high dimensions, three questions from Paul Erdos's published list of open problems, and results in group theory, operator algebras, quantum complexity and lattice cryptography.
Claims like this are normally impossible for an outsider to check, which is why they tend to be argued about rather than tested. Our reading is that the public Lean files make this release unusually inspectable: a reader can download and check the final artifacts, even though Astra's discovery process cannot be rerun. Alongside the announcement OpenAI released each argument as a file written in Lean, a language in which every step of a proof is stated precisely enough that a computer can confirm it follows from the step before it. The files are public, carry an open licence, and anyone with the software installed can run them.
So we did. The ten certificate files contain 548,205 lines of Lean; counting the ten-line All.lean aggregator that imports them brings the top-level project total to 548,215. In that language, an author who wants to leave a step unproved writes the word sorry in its place, and the machine will still accept the proof with a warning attached. We searched the ten top-level certificate files for that word and found no matches. The separate ComparatorChallenges fixtures in the same repository do contain placeholders, so this is not a repository-wide zero. OpenAI's own summary file records no unproved steps in the ten formalizations, and lists only the three standard assumptions that ordinary Lean mathematics is built on, with nothing added for the occasion.
On who did what, OpenAI is unusually direct. Its announcement says the results "were achieved by an internal version of Astra, our next major model", that the arguments "were then prepared into manuscripts by humans with the same model", and that afterwards "the model formalized each argument in a Lean certificate". Further down it writes that the company takes responsibility for the proofs being correct "while the mathematical arguments themselves were generated by our system". Beyond that paragraph, the division of labour is not spelled out anywhere.
The figure that travelled fastest was the price. OpenAI says the tokens needed to find all ten solutions "would cost roughly $2,000 at Sol API rates". That sentence is worth reading slowly. It is OpenAI's estimate of what the solution-search tokens would cost at Sol API rates. It is not the cost of building Astra, and the release does not disclose an all-in cost or say exactly which failed attempts, if any, are included.
The headline result concerns sphere packing, the question of how much of a space you can fill with balls of equal size. The paper reports the first improvement since 1978 to the general exponent for high dimensions, moving it from 0.59905576 to about 0.6044. In plain terms that is a tighter ceiling on how densely spheres could ever be packed, not a better way of packing them. Nobody built a new arrangement. What improved is the limit on what any arrangement could achieve. Elsewhere OpenAI says the work resolves Erdos problems 146, 180 and 183, though the independent Erdos Problems catalogue still listed all three as open on 5 August. The ten also construct what is called a non-sofic group, answering a question Weiss asked in 2000 about a property Gromov had introduced the year before.
What the machine check does not cover matters as much as what it does. Lean confirms that the formal statement follows from the formal definitions written down beside it. It cannot confirm that those definitions mean what the English sentence in an announcement means, and it says nothing at all about whether a result is important. No peer-reviewed publication of any of the ten had been identified by 1 August. The papers thank several named specialists for their comments, which is consultation rather than independent certification.
One detail that almost no coverage picked up sits in the acknowledgements. While the paper was being written, its authors learned of independent and concurrent work by Shuoxing Zhou reaching one of the same conclusions, a counterexample to Connes's rigidity conjecture, "developed in part with the assistance of GPT-5.6 Sol". A person got there at the same time, also with a model's help.
That is the shape of it. Ten claims, arriving with unusually inspectable evidence attached, and with the most important judgement still missing. Whether these results matter, and whether the formal statements capture the questions mathematicians actually care about, is not something a computer can settle. That part belongs to the mathematical community, and it has not spoken yet.
Original source: OpenAI