A model reveal through formal mathematics

The competitive bar for reasoning models is moving from benchmark answers toward research artifacts that others can inspect. OpenAI researcher Noam Brown wrote on X that "An internal version of Astra, @OpenAI’s next major model family, solved 10 major open problems" in mathematics, quantum complexity, and theoretical computer science. The source post is available on X.

The linked OpenAI publication gives the claim its substance. Dated August 1, 2026, it lists 10 results on problems that OpenAI says had seen no progress on the main result for at least a decade in most cases. The topics include high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes’s rigidity conjecture, arithmetic circuit lower bounds for the permanent, quantum parallel repetition, closest vector problem hardness, Ehrhart’s volume conjecture, multicolor Ramsey numbers, and extremal graph theory.

The concrete number is unusual: OpenAI says the total token budget needed to find the solutions would cost roughly $2,000 at Sol API rates. The arguments were then prepared into manuscripts by humans with the same model, and each was formalized as a Lean certificate. The accompanying openai/ten-proofs GitHub repository contains Lean 4 formalizations and build instructions, including files such as NonSoficGroup.lean, Permanent.lean, and SpherePacking.lean.

Brown’s account is a high-signal channel for OpenAI reasoning work, and Sam Altman reposted the item. The next question is not simply whether the proofs compile. Mathematicians will need to evaluate novelty, attribution, problem framing, and whether future Astra outputs can be reproduced with enough prompt and trace detail to become a normal research workflow.

#lean

Astra turns 10 open problems into Lean-checked research claims