OpenAI Unveils Ten Mathematical Results Produced by Astra, Opens Lean 4 Certificates for Independent Reconstruction

OpenAI has announced ten results in mathematics and theoretical computer science produced by an internal version of Astra, spanning high-dimensional sphere packing, coding theory, group theory, arithmetic circuit complexity, quantum parallel repetition, lattice-based cryptography, and extremal combinatorics. The company says the model first discovered the arguments, after which humans worked with the same model to organize them into manuscripts totaling 249 pages. The model then formalized each argument as a Lean 4 certificate.

More specific claims include advancing the asymptotic upper bound for general high-dimensional sphere packing to the Cohn–Elkies linear programming threshold; constructing a non-sofic group; producing a counterexample that disproves the Connes rigidity conjecture; proving an Ω(n⁴/log n) arithmetic formula lower bound for the permanent; and establishing n^(1/400)-factor hardness of approximation for the Euclidean Closest Vector Problem. OpenAI also claims to have solved two Erdős problems in extremal graph theory and obtained a superexponential lower bound for multicolor triangle Ramsey numbers.

Unlike releases containing only natural-language solutions, the `openai/ten-proofs` repository provides ten corresponding `.lean` modules and pins Lean 4.32.0, mathlib, and Lake. Researchers can first obtain the mathlib cache and then run `lake build All` to reconstruct all formalizations. A Comparator challenge is also included to reduce the risk of false axioms, undeclared assumptions, or untrusted shortcuts entering the proof chain. OpenAI estimates that the tokens consumed while searching for these solutions would cost about $2,000 at Sol API rates, but it has not released Astra’s weights, complete search traces, failed samples, or actual compute usage.

Acceptance of a certificate by the Lean kernel means only that the formal statement can be derived from the specified dependencies. It does not automatically prove that the formalized proposition is fully equivalent to the original public problem, nor can it replace checks for novelty and prior results in the literature. The next step is to see whether researchers in the relevant fields can independently reconstruct the proofs, verify the definitions, and identify any earlier results. Until then, the ten results should be regarded as major research claims accompanied by machine-verifiable artifacts, rather than peer-reviewed conclusions.