OpenAI publishes ten mathematical results
An internal version of Astra closed or substantially advanced ten long-open problems across eight fields; the tokens needed to find every solution would have cost about two thousand dollars.
Why it matters
A single result became a rate: ten open problems, each formalised in Lean, at a cost that can be stated as a number.
The publication is dated 1 August 2026. The results span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. Among those named: new upper bounds on sphere packing density up to the Cohn-Elkies bound; exponentially improved bounds for binary and high-dimensional spherical codes; a construction proving the existence of non-sofic groups; a refutation of Connes's rigidity conjecture; a lower bound of order n to the fourth over log n for arithmetic formulas computing the permanent; an exponential parallel repetition theorem for general two-player quantum games; the approximation hardness of the closest vector problem; the Ehrhart volume conjecture; and a super-exponential lower bound for multicolour Ramsey numbers for triangles, resolving Erdos problem 183. At Sol API rates the tokens required to find these solutions would have cost approximately two thousand dollars. Humans then used the same model to write the proofs up as manuscripts, after which the model formalised each as a Lean certificate; a description of the model's reasoning is published for every solution.