OpenAI published a paper on Saturday setting out solutions to 10 problems in mathematics and theoretical computer science, and credited the mathematics not to any person but to an internal version of Astra, a model it has not released. Hours earlier, one of the 10, a construction in group theory, had leaked on X.
The figure that will get repeated is $2,000. That is what OpenAI estimates the tokens used to find all 10 solutions would cost at the API rates for GPT-5.6 Sol, its current flagship. Every problem on the list had gone at least a decade without progress on its main result, and most of them far longer.
The leak came first. Screenshots of the group theory chapter circulated overnight under the title "Nonsofic Groups Exist," and Elliot Glazer, lead mathematician at Epoch AI, replied that the pages were genuine and called the work the most important math AI result yet. The full publication followed the same morning.
The announcement's most consequential sentence is not about any theorem. OpenAI writes that "claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work." Until now, AI-assisted mathematics has been published under human names with the model in the acknowledgements. OpenAI's position is that its staff prepared the manuscripts and take responsibility for correctness, while the arguments themselves belong to the machine.
What the 10 results cover
The group theory item is the one that leaked, and it closes a question open since Benjamin Weiss named the property "sofic" in 2000. A group is a set of moves plus a rule for combining them, like the rotations of a Rubik's cube. Sofic means any finite piece of the combination table can be imitated, to any accuracy you choose, by shuffling a finite deck of cards. Every group anyone had tested passed, and until Saturday no counterexample was known.
The rest range well beyond group theory. The sphere-packing chapter claims the first improvement since 1978 to the general bound on how densely balls can fill high-dimensional space. Another disproves Connes's rigidity conjecture in operator algebras. One settles Erdős problem 183. One proves new hardness for the closest vector problem, a lattice question sitting underneath post-quantum cryptography.
What can be checked and what cannot
Unlike July, the work arrives with the machinery to check it. OpenAI released the manuscripts, a narration of the model's reasoning, and a Lean certificate for each argument. A Lean certificate is a proof written so a computer can verify every step, which rules out the quiet gaps that sink most claimed proofs of famous conjectures. It does not establish that the formalized statement is the conjecture mathematicians care about, and it is not peer review.
The July precedent is worth holding onto. OpenAI attributed a proof of the Cycle Double Cover Conjecture to GPT-5.6 Sol Ultra on July 10, and Jim Geelen and Sang-il Oum separately wrote up expositions of that argument. Wolfram MathWorld records that the claim had not reached a refereed publication by the end of the month. Verification runs on months, not news cycles.
OpenAI is not alone in this either. A counterexample found with Anthropic's Claude Fable 5 ended the 87-year-old Jacobian Conjecture in three variables, and Terence Tao worked through it publicly on July 21.
What OpenAI has that its rivals do not is a model nobody outside the company can test. Sam Altman spent this week previewing the Astra family in Washington, where it was pitched for work that runs across hours or days and multiple agents rather than a single answer. It has no release date, no benchmark scores, no price and not even a settled name, and the $2,000 is an estimate at a different model's rates.
Sébastien Bubeck, who works on AI at OpenAI, marked the release by noting that he had expected AI to beat him at mathematics by 2030 and got 2026 instead. The company's own reported numbers have needed unpacking before, as with its 38.3% self-reported ARC-AGI-3 result. This time it handed over the proofs, the Lean files and the reasoning traces. The next move belongs to the mathematicians.