OpenAI Dropped 722 AI-Generated Math Manuscripts on GitHub You Can Actually Check

An unreleased frontier model produced formal proofs spanning 372 problem families—and for once, the verification harness ships with the claims.

The interesting number isn’t 722. It’s zero—as in the number of these proofs you’re being asked to take on faith.

That’s the part almost everyone covering this is skating past. The story being told today is the obvious one: an unreleased frontier model produced 722 manuscripts spanning 372 families of long-standing mathematics problems, OpenAI put them on GitHub, and depending on your temperament this is either the machines arriving at the summit of human reasoning or hype dressed up in formal notation. Both readings are wrong, or at least badly incomplete. The headline isn’t that a model did mathematics. The headline is that, for once, the claim ships with its own verification harness—and that single design decision changes how you should read everything else.

Give the breakthrough narrative its due first

Let me steelman the excited reading, because it’s not stupid. “AI solved a bunch of hard math” has been a press-release genre for years, and it has almost always meant one of three things: the model restated a known result, the model produced plausible-looking prose that a human had to fix, or the benchmark was quietly curated so the model couldn’t lose. You could not check any of it. You read the blog post, you squinted at the cherry-picked example, you moved on.

This is different in a way that matters. Formalizing a proof in Lean means the statement and every inferential step are encoded in a language a proof assistant mechanically checks. There’s no “the rest follows by standard arguments.” Either the kernel accepts the term or it doesn’t. So when the output is a Lean development rather than a PDF of confident paragraphs, the usual escape hatches close. The excited crowd is right about this much: a machine-checkable corpus at this volume is a genuine step up from the vibes-based math demos we’ve been fed. Concede it. It’s real.

And the scale isn’t nothing. 372 result families, whatever their individual difficulty, is a lot of surface area to formalize without a human spending a career on the Lean plumbing. If even a meaningful fraction hold up under scrutiny, that’s a useful artifact for anyone who works in formal methods.

Now here’s what that reading gets wrong

The number 722 is doing enormous rhetorical work and deserves none of it. Manuscripts aren’t theorems, result families aren’t uniform in difficulty, and “long-standing” is a word that collapses a spectrum from “genuinely open and famous” down to “unformalized but well understood for decades.” A corpus can be simultaneously large, verified, and mathematically modest. Counting manuscripts tells you about throughput, not depth. Treat the big number the way you’d treat a lines-of-code metric: a sign of activity, not of value.

More importantly, the thing being celebrated—the Lean layer—is also the thing that pins down the ceiling. A proof assistant verifies that a proof follows from a statement. It cannot tell you the statement is the interesting one, or even the one you meant. All the trust in a formal development lives in two places: the theorem statement and the axioms it leans on. The proof body is the part you don’t have to trust, because Lean checked it. The parts you still have to trust are exactly the parts a machine can’t check.

So the correct way to review this release is almost the opposite of how people are reacting to it. Nobody needs to read the proofs. You need to read the statements and audit the axioms.

Review it yourself—the right way

Clone the repository linked from the announcement and build it. If it’s a standard Lean 4 project, that’s the usual toolchain:

1
2
3
4
5
6
7
8
9
10
11

# grab the Lean version manager if you don't have it
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
​
git clone <repo-url-from-the-openai-post>
cd <repo>
​
# fetch cached builds of dependencies (mathlib is huge; don't compile it yourself)
lake exe cache get
​
# this is the real test: does the kernel accept everything?
lake build

If lake build completes clean, the kernel has accepted every term. That’s necessary but not sufficient, because a proof of a trivial or malformed statement also builds clean. Two checks separate a real result from a dressed-up tautology.

First, hunt for the escape hatches. A development that “builds” can still be riddled with holes if it uses placeholders:

1
2
3
4
5

# any of these means a step was asserted, not proved
grep -rn --include='*.lean' -E '\bsorry\b|\badmit\b|\bnative_decide\b' .
​
# custom axioms are where unproven assumptions hide
grep -rn --include='*.lean' -E '^\s*axiom\b' .

Second—and this is the check almost nobody runs—interrogate the axioms each headline theorem actually depends on. Lean will tell you:

1
2

-- at the bottom of the file, for each result that matters
#print axioms someHeadlineTheorem

You want to see the three standard foundations and nothing else: propext, Classical.choice, Quot.sound. If a result also depends on a project-local axiom, the “proof” is conditional on an assumption someone asserted by hand. That’s not fraud—conditional results are legitimate—but it is a very different claim from “we proved this,” and it won’t show up unless you look.

Then, and only then, read the theorem statement in plain Lean and ask whether it says what the manuscript claims it says. A proof of ∀ n, P n → P n is airtight and worthless. The gap between the English summary and the formal statement is where every inflated claim I’ve ever audited actually lived.

The unsettled mathematicians aren’t being precious

Part of the mathematics community is impressed, part is uneasy, and the easy move is to wave that off as professional self-preservation. Don’t. The unease is pointing at something the cheerleaders aren’t.

A machine-checked proof is correct by construction and frequently illegible—a mountain of term-rewriting that certifies truth without conveying understanding. Mathematics has never been only about establishing that a statement is true. It’s about why, about the structure that makes a result inevitable, the idea you carry to the next problem. A corpus of 722 verified-but-opaque developments can advance the ledger of known-true statements while contributing roughly nothing to the thing mathematicians actually trade in. That’s a legitimate worry about the kind of knowledge being produced, not a status-anxiety tantrum. It deserves a straight answer, and “but it compiles” isn’t one.

Verified and understood are different properties. A proof assistant guarantees the first and is completely indifferent to the second.

What the unreleased-model framing is quietly costing you

Here’s the part that should temper everyone, optimist and skeptic alike. The model that produced this isn’t available. You cannot hand it a new problem family and watch what happens. So the one experiment that would actually calibrate its ability—novel inputs, no retries, nobody curating the wins—is exactly the one you can’t run. You get the outputs and the verifier. You don’t get the process, the failure rate, the number of attempts behind each success, or the amount of human scaffolding in the loop.

That’s why the Lean layer is both the best and the most convenient part of this release. Best, because the results that are there are genuinely checkable and that’s rare and good. Convenient, because a wall of verified proofs invites you to extrapolate from a curated highlight reel to a general capability, and the formal rigor of the artifacts lends false rigor to that leap. Verified outputs tell you nothing about the base rate. A model can be astonishing on the problems it solved and useless on the ten it didn’t, and a highlight reel looks identical either way.

So do the unglamorous thing. Clone the repo. Run lake build. Grep for sorry. Print the axioms on the results that would matter if true. Read the statements against the claims. Treat what survives as real and interesting—because some of it will be—and treat the 722 as a throughput figure, not a verdict.

The machines didn’t just do frontier mathematics. They did something narrower and, honestly, more useful: they shipped claims you can falsify before breakfast. Go falsify a few.