On August 1, 2026 OpenAI published a selection of ten results that each resolve or make substantial progress on a long-standing open problem in mathematics or theoretical computer science. The problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. OpenAI states the results were achieved by an internal version of Astra, which it describes as its next major model, and that the total number of tokens needed to find the solutions would cost roughly 2,000 dollars at Sol API rates.
The named results include new upper bounds on sphere-packing density down to the Cohn-Elkies threshold; exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance, with analogous results for high-dimensional spherical codes; a construction establishing the existence of non-sofic groups; a disproof of Connes’s rigidity conjecture; an arithmetic-formula lower bound of order n to the fourth over log n for computing the permanent; an exponential parallel repetition theorem for general two-player quantum games; polynomial-factor hardness of approximation for the closest vector problem; a determination in every dimension of Ehrhart’s volume conjecture; a superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdos problem 183; and results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdos problems 146 and 180.
The workflow matters as much as the results. The model generated the mathematical arguments; humans then prepared those arguments into manuscripts with help from the same model; and the model afterward formalized each argument in a Lean certificate. OpenAI released the Lean certificates in a public repository, created on August 5, 2026, along with a narration of the model’s thinking process for each solution. That combination means an outside mathematician can machine-check the claims rather than take the lab’s word for them, which is a materially different verification posture than a press release with a summary chart.
On attribution, OpenAI wrote 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. It says it helped prepare the manuscripts and the Lean formalizations and takes responsibility for their correctness, while the mathematical arguments themselves were generated by its system. The post explicitly acknowledges the signers of the Leiden declaration on AI and Mathematics, and notes that the May 2026 disproof of the Erdos unit-distance conjecture has already prompted follow-on papers by human researchers.
For a leader, the number to watch is not the count of theorems but the cost. Roughly 2,000 dollars of inference produced ten research-level contributions in fields where a single result can be a career milestone, and two of the areas touched — closest-vector hardness and coding theory — sit directly under post-quantum cryptography and communications engineering. Formal peer review of these results has not happened yet, so the appropriate stance is to treat the Lean certificates as the evidence and the journal record as still outstanding.