OpenAI has named its next major model, Astra, by publishing ten mathematical results it says were generated by an internal version of the system. The company released a technical paper, reasoning walkthroughs and Lean certificates that allow the formal proofs to be checked by software.
The more important part of the announcement is not the count. AI-generated mathematics has produced enough false starts that a headline number alone is weak evidence. OpenAI's decision to publish machine-checkable certificates gives researchers something concrete to inspect, although it does not remove the need for human review.
What Astra produced
The ten results cover high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics.
Among them is a construction establishing the existence of non-sofic groups, addressing a question in group theory that had remained open since the concept was introduced in 1999. Astra also produced a counterexample to Connes's rigidity conjecture, new bounds for sphere packing and error-correcting codes, and an exponential parallel repetition theorem for two-player quantum games.
Three results address problems from Paul Erdős's catalogue: multicolor triangle Ramsey numbers and two conjectures in extremal graph theory. Another concerns the closest vector problem, a lattice question with relevance to post-quantum cryptography.
OpenAI says the tokens used to find all ten solutions would cost roughly $2,000 at its Sol API rates. Humans then worked with the same model to prepare manuscripts, after which the model formalized each argument in Lean.
Verification is the real test
Lean checks whether a formal proof follows from its stated definitions and axioms. That makes the certificates reproducible in a way that conventional prose proofs are not: OpenAI has published the files in a public GitHub repository, where others can run them through Lean's kernel.
A successful build is not the end of the review. It verifies the formal statement encoded in Lean, not automatically that the statement matches the original open problem as mathematicians understand it. Researchers still need to inspect the formalization, judge the significance of each result and determine whether related work changes the novelty claims.
That distinction matters because OpenAI has previously faced scrutiny over AI-generated mathematical claims. Publishing the proofs, formal certificates and reasoning records together gives the mathematical community a substantially better audit trail this time.
Astra remains unavailable
OpenAI describes Astra only as its "next major model" and has not announced an API, release date, pricing or system card. The publication therefore demonstrates a research capability, not a product developers can test.
The company also addressed attribution directly. It says the mathematical arguments came from Astra, while its researchers prepared the manuscripts, helped formalize the proofs and accepted responsibility for their correctness. OpenAI cited the Leiden Declaration on AI and Mathematics, which argues that researchers should disclose AI contributions rather than claim human authorship for machine-generated work.
The ten results now move into a slower process than model evaluation: independent mathematical review. Lean narrows the verification problem, but it does not settle questions of framing, novelty or importance. Those judgments remain with the field.
Sources
OpenAI: Ten advances in mathematics and theoretical computer science
