OpenAI Cited the Declaration That Warned About This

Ten proofs. About 2,000 dollars in tokens. The strongest verification any machine-produced mathematics has cleared, and three questions it still leaves open.

On August 1, OpenAI published ten new results in mathematics and theoretical computer science. Each one answers a problem that had seen no progress on its main result for at least a decade, and in most cases far longer. The arguments were produced by an internal version of Astra, which OpenAI describes as its next major model.

The number everyone repeated was the price. OpenAI put the tokens needed to find all ten solutions at roughly 2,000 dollars at Sol API rates. That number is doing a lot of work in a lot of arguments this week, and it deserves a closer look.

But the part that matters for anyone shipping with frontier models is not the price. It is that every argument came with a machine-checkable Lean certificate. You do not have to trust OpenAI. You can run the checker. That single property changes what a claim costs to evaluate, and it is the thing worth stealing.

It also has a hard edge. Two months before any of this shipped, roughly 3,400 mathematicians signed a document naming the precise gap that a Lean certificate does not close. OpenAI linked to that document in its own announcement.

Ten results, one repository, three artifacts

The release has three parts. A 249 page manuscript collecting the ten arguments. A second document in which the model narrates how each solution came together. And a public repository of Lean 4 formalizations, one file per result.

The workflow OpenAI describes is worth reading carefully, because the division of labor is unusual. The model generated the mathematical arguments. Humans, working with the same model, turned those arguments into manuscripts. Then the model formalized each argument into Lean. OpenAI says it takes responsibility for correctness while attributing the arguments themselves to the system.

The results span high-dimensional geometry, coding theory, group theory, operator algebras, arithmetic circuit complexity, quantum complexity, lattice cryptography, and extremal combinatorics.

Trust moved from the producer to the artifact

In May, when OpenAI announced a machine-generated disproof of the Erdős unit-distance conjecture, the validation was social. Outside mathematicians read the argument and vouched for it. That is a strong signal, but it does not travel. To repeat the check you need the same expertise, and the check is a judgment rather than a result.

A Lean certificate is a different kind of object. Lean has a small trusted kernel. Feed it the formalization and it returns a binary verdict: the proof term type-checks against the stated theorem, or it does not. No credentials required. The repository pins its environment to Lean 4.32.0 with mathlib, so the check is reproducible by anyone with a laptop and the toolchain.

The repository goes further than most formalization releases. Its manifest declares which axioms the development relies on, and the list contains three entries, all of them the standard foundations that come with the library. Nothing exotic was assumed to make the proofs go through. The repo also ships configurations for checking the exported proofs with a second, independent kernel.

What a kernel check actually certifies

Here is the part that gets skipped in most coverage. A successful kernel check establishes that the encoded conclusion follows from the encoded definitions and assumptions. That is all it establishes.

It does not establish that the formal statement faithfully captures the historical conjecture. It does not catch a definition that quietly weakens the problem into something easier. It does not judge whether the theorem matters. Those are review questions, and they are answered by people who know the field, on a timeline measured in months.

So the certificate is real and the certificate is narrow. Both at once.

Ten wins, zero published failures

Ernie Davis, writing to Gary Marcus, asked the question that decides how impressed to be: how many conjectures were attempted? If ten were picked at random from the space of open problems and Astra closed all ten, that is astonishing. If fifty were picked because they looked tractable and ten landed, that is still notable and considerably less astonishing. If the model was run against every open Erdős problem and a thousand others, the failures are the more informative number.

The 2,000 dollar figure has the same shape. It is the token cost of finding the solutions that worked. It is a safe assumption that it excludes the runs that went nowhere, and it certainly excludes the salaries of the research staff who picked the problems, prepared the manuscripts, and shepherded the formalizations.

To OpenAI's credit, one of its own researchers said the quiet part out loud. Noam Brown noted that the effort produced "no Millennium Prize Problems (yet)" and added that they had not spent heavily on any single problem, leaving room to push test-time compute much further. That is a more honest framing than most of what circulated on X.

Reception among mathematicians has been split rather than dismissive. Thomas Bloom, who maintains the Erdős problems database, called the results big news and rated them significant as constructions, while rejecting the idea that any of this replaces mathematicians. Henry Yuen, reviewing the write-up of one result, found the prose characteristic of model-generated proofs: heavy on setup, casual at the point where the difficulty actually lives.

Written in June, describing August

In its announcement, OpenAI links to the Leiden Declaration on Artificial Intelligence and Mathematics, published on June 2, 2026, endorsed by the International Mathematical Union, and signed by several thousand mathematicians including Terence Tao, Peter Scholze, and Kevin Buzzard. OpenAI cites it while making an argument about attribution: that claiming human authorship for a machine-generated proof would misrepresent both the system and the nature of human intellectual work. On that specific point the company is aligned with the document.

What makes the citation interesting is the rest of the declaration. Its first listed threat is that automated techniques produce plausible but unreliable arguments that are hard to distinguish from correct proofs, and it says explicitly that this applies to formalizations too, because the difficulty sits in the translation between the computer-encoded statement and the human concept it is supposed to represent.

That is Figure 3's right column, written by mathematicians two months before Astra existed publicly. Its fourth threat covers results announced through blog posts on market timelines, ahead of community evaluation. And its recommendations for policymakers include a section headed "don't believe the hype", advising governments to consult mathematicians rather than press releases. That recommendation was published nine weeks before Sam Altman demonstrated Astra to officials in Washington.

The fair reading is not that OpenAI ignored the document. It published a full manuscript rather than a bare press release, released the reasoning narrations, formalized everything, and named the division of labor. The uncomfortable reading is that a checked proof and a checked claim are different objects, and the mathematical community said so in advance.

Astra is a name, not yet a model you can call

If you are planning around this, keep the two stories separate. The proofs are a capability demonstration from an internal build. Astra as a shipping product is barely specified.

One caution on the long-running design. The known weakness of multi-agent setups is compounding error as context grows, and prior work has found that coordination overhead can make additional agents actively worse on tightly coupled tasks like planning. Mathematics is an unusually forgiving domain for this architecture, because a proof attempt either verifies or does not. Most production workloads do not behave that way.

Four things to take into your own stack

The ten arguments are in the open, formalized, and rebuildable by anyone who wants to spend an afternoon on it. That is a genuinely higher bar than the industry has cleared before. It is also the easy half. The half that decides what this release means is the one no kernel can compute, and it belongs to people who will take months to answer.