OpenAI drops 722 math manuscripts, won't say how many are verified

A repo appears at 21:47 UTC

On October 6 at 21:47 UTC, a repo called openai/math shows up on GitHub. Inside: 722 math manuscripts, all produced by an internal OpenAI model nobody outside the company can touch. Fourteen minutes later, the last file lands. By the next day, the repo has cleared 8,500 stars.

Coverage splits over two different numbers. The Decoder leads with 372 results, unite.ai with 722. Both are right, and the README reconciles them in one line: "722 manuscripts organized into 372 families."

A family bundles the papers that orbit the same result: its main argument, its consequences, its alternate proofs. Counting families versus papers is counting box sets versus individual discs.

The word that replaced the number

What neither 722 nor 372 answers is the question that actually matters: how many of these proofs can a machine actually check?

OpenAI's announcement doesn't say. It shares "formalizations of many of the proofs in Lean," a language that lets a computer verify a mathematical proof step by step. Many. The word is doing the job a number should be doing, like a label promising fruit without printing the percentage.

Formalizing means rewriting a proof in a language where the computer grants nothing: no intuition, no "it's easy to see that." Skip one step and it simply won't compile. That's why this one count matters more than any other number in the repo: it's the only figure that says anything about how solid the batch actually is.

Both outlets split over 722 and 372 copied that "many" word for word, without ever running the count themselves: the argument was over the decorative number, not the one that actually settles anything. One specialist outlet did go looking, found a number, and published it with the file it came from. That file, it turns out, doesn't tell the whole story.

We've written here before about what that kind of verification is worth: on September 8, it was a single Lean-checked proof that kept an announcement from being dismissed as just another take on a question that had sat open since 1934.

162, and why that's not 44%

One file answers the question: lean/formalization.yaml, version 0.4, whose own header describes it as a "Catalog of papers with a formalized main result." It holds 162 entries, each pointing to one manuscript.

162 out of 722 manuscripts is 22%, as of October 7. The date matters: the file is versioned, and OpenAI says it plans to keep adding to it.

A flashier ratio is already making the rounds: 162 out of 372 families, or 44%. It's wrong, and not by a little. Those 162 entries name papers, not families, and 23 families carry more than one: family 331 alone accounts for 7 formalized papers. Putting papers in the numerator and families in the denominator is dividing apples by crates.

The family-level count has been done: those 162 papers cover 127 of the 372 families, or 34% at the same snapshot.

The official catalog is missing proofs

But the repo carries a second ledger, and it tells a different story. In the manuscript index, 235 of the 372 families link out to a page describing the scope of their Lean formalization, and the folder hosting those pages holds exactly 235 files. The catalog itself only covers 127.

That leaves 108 families with a Lean scope page and no matching entry in the formalized-results catalog. The reverse never happens.

Take family 005, the irrationality of Catalan's constant. Its page is unambiguous: "The formalization proves that Catalan's constant ... is irrational. This is the mathematical assertion in the paper's title." The file Catalan.lean is sitting right there, and the word "Catalan" never appears in formalization.yaml.

Twelve of those 108 pages were opened one by one. All twelve describe a formalization of the actual main result, from the irrationality exponent of pi to Erdős's reciprocal-sum conjecture. These aren't placeholders.

So 162 is a floor: the official ledger is shorter than the shelf it claims to describe.

"Formalized" doesn't mean "verified"

There's one more gap, running the other direction. Some coverage already treats the 162 proofs as "verified by Lean." Nobody has published a verification.

What OpenAI actually ships is 405 statement files and instructions for checking them yourself. The repo carries no continuous integration: nothing runs automatically, and the Lean library's own README warns that compiling everything at once can fail, adding "we recommend compiling only small portions at a time." OpenAI hands over the sealed envelope and the letter opener, and leaves it at that.

We haven't opened it either: we counted files and read OpenAI's scope descriptions, but we haven't compiled a single proof. And those 405 files aren't 405 results, either, since one family alone can claim four of them.

Of the 560 manuscripts with no catalog entry at all, OpenAI includes a line that most coverage left out: "Some of the unformalized results could have issues."

The two outliers

The README spells out the production line: roughly 4,000 problems fed to the model, about three hours of ChatGPT Pro thinking per result, and a filtering pass that left this particular catalog standing.

Two results break that pattern, and the document says so in plain language: the zero-free region of the Riemann zeta function and the Hodge conjecture for CM abelian varieties are flagged as "exceptions to this fixed procedure." For the zeta result specifically, OpenAI adds that the writeup was "human edited for readability." The two most prestigious results in the whole batch are, in other words, the two whose production looks the least like everything else in it.

The committee cited for cover published the opposite of an endorsement

OpenAI says it drew on the public recommendations of an independent advisory group on mathematics and AI, based at the Institute for Advanced Study, in shaping this release. That same day, the group published its own statement on the release, opening by refusing to be read as a sign-off: "AGMAI's advisory role should not be interpreted as a judgment of the impact of these results or an endorsement of the process by which OpenAI obtained them."

It adds that this release is "the beginning, not the completion, of the process of human understanding," and that it's up to the math community to judge it from here. It credits constructive discussions and OpenAI's willingness to engage.

There's a sharper line still. Its September 29 recommendations, the very ones the announcement invokes, open with a request this release doesn't honor: "we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models." The 722 manuscripts come from exactly that: an unpublished, internal, proprietary model. OpenAI says it is working to release it.

Its nine members aren't paid. They built this independent body after OpenAI approached some of them about joining an in-house committee instead. Fields medalist Timothy Gowers and Edward Witten both sit on it.

Don't confuse this nine-person committee with the statement signed by twenty-five Fields medalists on September 11, which we've also covered here: that document names no company and takes no position on whether any proof holds up. Two documents, two different scopes, with exactly one man in both: Martin Hairer, the 2014 Fields medalist, who signed the declaration and also sits on the committee. Not objecting isn't the same as approving, and being cited isn't the same as vouching.