OpenAI attributes ten mathematics advances with Lean certificates to Astra

On August 1, OpenAI published an unusual capability claim: an internal version of Astra, its next major model family, produced new results on ten problems in mathematics and theoretical computer science. They are not all “ten solved problems” in the same sense. The collection includes resolutions of conjectures, such as the existence of non-sofic groups and Ehrhart's volume bound, but also substantial partial advances, such as a better asymptotic sphere-packing bound and new bounds for codes and the complexity of the permanent.

The breadth matters. The papers span high-dimensional geometry, group theory, operator algebras, quantum complexity, lattices, and extremal combinatorics. The 249-page technical collection contains full statements and proofs, not a benchmark table. And Astra did not stop at drafting informal arguments: OpenAI published a repository of Lean formalizations for the main results.

That package makes the announcement materially different from “a model seems good at mathematics.” It also requires separating four layers of evidence that are often conflated.

What formal checking adds

According to OpenAI, Astra generated the mathematical arguments; people prepared the manuscripts with help from the same model; the model then translated each argument into a Lean certificate. The company does not claim human authorship of the ideas and publicly takes responsibility for the work's correctness.

Lean requires definitions, assumptions, and logical steps to be expressed in a language that a small kernel can check. The repository declares that its main formalizations contain no sorry—the marker for a missing proof—and limits them to three standard library axioms. In addition to building with Lean, every result includes a Comparator configuration with a second checker, Nanoda. That route lets a reviewer check that the solution proves the same public statement, introduces no unexpected axioms, and is accepted by more than one kernel.

The redundancy is not ceremonial. The project pins Lean 4.32.0, and version 4.32.1 fixed a kernel soundness bug. Lean's documentation says that the recommended Comparator route was not affected by that bug; OpenAI's configurations enable the additional checker. The lesson is not that the certificates are thereby invalid, but that “it compiles” should not end an adversarial audit. The public code makes it possible to replay the check with a smaller trusted base than the system that generated the proof.

This is a practical advance over February. In the First Proof challenge, OpenAI submitted ten informal attempts at research problems and later acknowledged, after external feedback, that one it had initially considered likely correct was wrong. In May, another internal model disproved Erdős's unit-distance conjecture, and the proof was checked by external mathematicians. The company is now trying a third route at batch scale: readable argument, public formalization, and tools for independent replay.

What Lean does not decide

A formal certificate checks exactly the theorem it has been given, within the definitions it has been given. It does not by itself decide that the statement faithfully represents the conjecture expressed in ordinary mathematical language. Nor does it establish that a result is new, important, or clearly explained, or review the bibliography. Those connections belong to the specification and still require domain experts.

That distinction is especially important in such a heterogeneous collection. An expert in sphere packing cannot validate the quantum repetition result by extension; every chapter needs a different community. The repository's own metadata currently labels the review as agent-conducted. OpenAI has supplied far more than a press release, but the manuscripts have just appeared and are not equivalent to ten independently refereed papers.

The reasoning walkthroughs are not a raw discovery record either. Their abstract explains that another model read the original chains together with the finished papers and reconstructed how the ideas came together, including detours and failed approaches. They are useful for understanding the proofs; they do not fully audit what Astra was instructed to do, how many candidates it explored, or how much selection work people performed.

That omission changes how the most striking economic number should be read. OpenAI estimates that the tokens needed to find the successful solutions would cost roughly $2,000 at Sol API rates. This is not the total cost of the result: it excludes training Astra, the universe of problems or discarded attempts, the human work of preparing 249 pages, formalization—which the public record logs as one week—and review. Without that denominator, the figure shows that a successful run can be cheap; it does not measure the chance of obtaining one or make the system's productivity reproducible.

My reading is that the advance would remain important even if independent review found errors in part of the collection. A correctable proof is not worth the same as a correct one, but the relevant capability here is a broader chain: sustaining arguments across very different fields, converting them into enormous formal objects, and exposing them to public checking. If several results survive, the bottleneck in some areas may shift from proposing a proof route to choosing questions, formalizing their meaning well, recognizing valuable ideas, and reviewing a growing volume of results.

That change should not be extrapolated without limits. Mathematics offers an exceptional verification signal: a checker can reject an invalid step without performing a physical experiment. In biology, chemistry, or medicine, a coherent derivation does not replace new data or clinical outcomes. Astra is also unavailable to outside labs, so today the certificates can be reproduced, but the discovery capability that produced them cannot.

The Leiden Declaration on AI and Mathematics defends independent verification, attribution, and community judgment at the same time. This release partly responds with proofs, code, and explicit attribution to the system. It retains another tension: the arguments are open, but the model, selection process, and full workflow remain proprietary.

That is the frontier worth following. The event is not that Lean automatically converted ten announcements into truth, or that Astra replaced mathematicians. It is that a lab has released a batch of contributions that no longer asks us to trust only the model's eloquence. The community can now separate logical correctness, fidelity of the statement, novelty, and value. For an AI meant to expand knowledge, that separation is part of the result, not a later formality.

Sources

• OpenAI, Ten advances in mathematics and theoretical computer science, August 1, 2026.
• OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, technical collection, August 1, 2026.
• OpenAI, ten-proofs repository and Lean certificates, accessed August 3, 2026.
• OpenAI, How the Ideas Came Together: Mathematical Discovery Notes, August 1, 2026.
• Lean, Validating a Lean Proof and Lean 4.32.1 release notes, accessed August 3, 2026.
• OpenAI, Our First Proof submissions, February 20, 2026.
• OpenAI, An OpenAI model has disproved a central conjecture in discrete geometry, May 20, 2026.
• Leiden Declaration on Artificial Intelligence and Mathematics, June 2, 2026.