OpenAI Published 722 Maths Manuscripts. 162 Have Lean Proofs.

OpenAI dropped a repo called openai/math on October 6 and it took 8,839 stars in a day. The posts carrying it said 300 solutions and claimed proofs of the Hodge Conjecture plus something about the Riemann zeta function. The repo says different numbers.

It holds 722 manuscripts in 372 families, written by an unreleased internal model at roughly three hours of thinking compute each, out of about 4,000 problems posed. 162 of those manuscripts have a Lean formalization. 560 don’t. OpenAI says so itself, in plainer language than anyone repeating it: results sit at different stages of verification and the unformalized ones could have issues.

The Hodge Conjecture result isn’t in the formalized list. The formalization catalogue’s own review field reads unchecked and its automation field says the formalizations were produced by an agent.

Best for anyone who saw the headlines and wants the actual state of it. Not ideal for anyone wanting a verdict on whether the maths holds, because nobody has that yet.

Here’s a number that does more work than any headline from yesterday.

That’s how many of the 722 manuscripts in openai/math come with a Lean formalization, counted out of the repo’s own catalogue file. The other 560 are PDFs.

That isn’t a gotcha. OpenAI wrote it down. The README says results sit at different stages of verification. It says not all of them have accompanying Lean formalizations. It says some of the unformalized results could have issues. Three sentences, sitting in the first screen of the repo page. What happened is that the careful version stayed in the README while a much louder version went around X.

So here’s what’s actually in there.

What Was Actually Released

A family groups related papers, so 722 manuscripts across 372 families averages 1.9 papers per result. A family can hold a principal result plus companion arguments, consequences or alternative proofs of the same thing.

The 4,000 figure is worth sitting with. Roughly 4,000 problems went in and 722 manuscripts came out, which is about 18%. OpenAI describes the filter as aggregating output into families and requiring an appropriate level of significance. What happened to the other 82% isn’t in the repo.

Apache-2.0 is doing more work here than a licence line usually does. Anyone can lift the Lean statements and the proof scripts into their own library without asking permission, which is how formal mathematics actually accumulates. A result nobody can reuse is a trophy. A result sitting in a permissively licensed Lean file is a brick other people build on top of.

Shipping it as a repo rather than a pile of PDFs has a second effect that’s easy to miss. A paper asks you to trust the author or wait for a referee. A repo asks you to run lake build and find out for yourself. That’s the whole difference between this release and every previous “AI did mathematics” moment, at least for the 162 of them that come with proofs.

What A Lean Proof Does And Doesn’t Settle

Lean is a proof assistant. You write a statement and a proof in a formal language, then the compiler checks every step against the axioms. If it compiles, the proof follows. No hand-waving survives it and no reviewer has to trust the author.

That makes openai/math different in kind from a model claiming it solved something. 162 of these can be checked by a machine, by you, today, with no mathematician required for the checking step.

Two things it doesn’t settle, both of which matter here.

The Statement Still Has To Match The Claim

Lean proves the formal statement you wrote. Whether that formal statement faithfully captures the informal theorem in the PDF is a human judgment and it’s where formalization efforts usually go wrong. A subtly weakened hypothesis compiles perfectly and proves something less than advertised.

The repo’s structure acknowledges this. Each formalized result carries a comparator config pointing at a specific declaration in a specific file, so a reader can see exactly which named theorem was checked. There are 185 such declarations against 162 papers. That’s the honest way to ship it.

560 Of Them Have No Formalization At All

The other 560 manuscripts are PDFs with LaTeX source. They get reviewed the old way, by people, slowly. OpenAI says it will keep adding formalizations as it obtains them, which means the 22.4% figure is a snapshot that should improve.

Until then, those 560 carry exactly as much weight as any unrefereed preprint. Which is some. Not none and not much.

The Hodge Conjecture Claim Isn’t In The Formalized List

This is the specific thing worth knowing, because it’s the claim that travelled furthest.

Posts yesterday said the release includes a proof of the Hodge Conjecture for CM abelian varieties. The repo does list that result and it names it as one of only two exceptions to the standard procedure. It is not in formalization.yaml. Searching the formalized titles for “Hodge” or “abelian” returns nothing.

So the headline result is one of the 560, not one of the 162.

The Riemann situation is stranger and worth getting right. OpenAI names its other exception as a zero-free region for the Riemann zeta function and specifies that the writeup for the Re(s) > 11/12 region was human edited for readability. Over in the formalized list sits a different thing: a paper titled “The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8”. Search the catalogue for “11/12” and you get nothing.

Two different regions, then. 7/8 is 0.875 and 11/12 is about 0.917, so the second is the stronger claim and it’s the one with no Lean proof attached and a human editing pass on the writeup.

We’re not going to tell you what either result implies. Zero-free regions for the zeta function are a specialist area. The distance between a small improvement and a breakthrough gets measured in fractions most people can’t eyeball. Anyone telling you otherwise after an afternoon on X is guessing. What we can tell you is which of the two a machine has checked.

The Catalogue Says Its Own Review Status Is Unchecked

Open lean/formalization.yaml and three fields near the bottom do more to set expectations than anything in the announcement.

status:
  scope: "Partial progress."

review:
  status: unchecked

automation:
  methods:
    - method: agent

Taken in order. The scope is partial progress, which matches 162 of 722. The review status is unchecked, meaning nobody outside has verified the catalogue’s claims about what it formalized. And the automation field says the formalizations themselves came from an agent rather than from human formalizers.

That last one deserves a second read. The manuscripts were written by a model. The Lean proofs checking some of the manuscripts were also produced by an agent. What a human did was build the harness and press go.

Which isn’t nothing. Writing Lean by hand is brutal work and the standing complaint about formalization is that it takes a specialist weeks to encode a result a referee could skim in an afternoon. An agent that emits compiling Lean at this volume is a real achievement on its own, separate from whatever the 722 papers turn out to say. It’s just an achievement about tooling rather than about mathematics. Those two get conflated constantly in the coverage, usually by people who’ve never watched a formalization project stall for a year on one definition.

None of that makes the proofs wrong. Lean doesn’t care who typed it, which is the entire point of a proof assistant: the compiler is the referee and it has no opinion about authorship. But “an agent wrote proofs that a compiler accepted” and “mathematicians have reviewed this” are different sentences and only the first one is currently true.

What The 162 Actually Cover

The Lean file paths tell you where the formalized work landed and it isn’t spread evenly.

Analysis takes 47 of the 185 declarations. Combinatorics has 28, geometry 27, probability 20. Computability gets 13 and number theory 11. After that it thins fast: algebra 7, group theory 5, linear algebra 5, algebraic geometry 4, information theory 4, ring theory 3, model theory 2, mathematical physics 2. Nineteen distinct areas in total.

Number theory sitting at 11 is worth noticing, given that the headlines were about the zeta function. The bulk of the machine-checked work is in analysis and combinatorics, not in the areas that made the posts.

A Third Of The Formalized Titles Are Counterexamples

Thirteen of the 162 formalized papers announce a counterexample in the title. A counterexample to Ryser’s covering conjecture, to Tachikawa’s second conjecture, to the group-ring determinant conjecture, to the infinite matroid packing and covering conjecture, to integer-degree harmonic dimension comparison.

That skew makes sense once you look at what a proof assistant is good for. Disproving a conjecture means exhibiting one object and checking it fails the property. That’s a finite, mechanical, checkable task and exactly the shape a formal verifier handles well. Proving a conjecture true means ruling out every possible counterexample, which is open-ended and much harder to mechanise.

So the formalized portion is weighted toward the kind of result a machine can nail down completely. That’s not a criticism of the work. It’s a useful signal about which claims from this repo are likely to stand up fastest.

The Kaplansky Family Shows What Good Looks Like

Four formalized papers cluster on Kaplansky’s conjectures: a counterexample to direct-finiteness in characteristic two, another in odd characteristic, a counterexample to the quasitrace conjecture with failure of tensor-product stable finiteness, plus work on the Bass trace conjecture and the characteristic-zero idempotent conjecture.

That’s a family in the repo’s sense and all of it carries Lean proofs. One of the ten published reasoning summaries covers the characteristic-two result, so you can read the model’s abridged reasoning next to the paper and then compile the proof yourself. Three independent views of the same claim.

Compare that to the Hodge result, where you get a PDF.

The Proofs Stand On Volunteer Work

The formalization catalogue lists 30 external Lean libraries that the project builds on. First is mathlib4, the community mathematics library that has absorbed something close to a decade of unpaid effort from hundreds of contributors.

The rest are more specialised and more telling. PrimeNumberTheoremAnd, a community project formalizing the prime number theorem and its surroundings. ClassFieldTheory. AINTLIB. strongpnt. A Lean formalization of the Rellich-Kondrachov theorem. A fixed-point theorems library. Each one is somebody’s side project, usually a single academic or a small group and each one is load-bearing here.

None of this diminishes what OpenAI shipped. It does reframe it. An agent produced Lean proofs quickly because the scaffolding it needed already existed, built by people who formalized the hard foundational material over years with no model to help them. The repo’s acknowledgements section thanks them by name, which is the right thing to do and also the clearest statement of what made the speed possible.

Worth holding onto when the next “AI did mathematics” headline lands. The checking infrastructure is the achievement that made the checking possible and volunteers built it.

The Ten Results OpenAI Chose To Show Its Work On

Alongside the manuscripts, OpenAI published abridged summaries of the model’s reasoning for exactly ten results. Which ten is itself informative, since it’s the sample they were most comfortable opening up.

Ordinary two-point correlations of multiplicative functions. The irrationality exponent of pi. The symmetric and general Mahler conjectures. Ordinary NP-hardness at the basic semidefinite threshold. Quasipolynomial bounds for arithmetic progressions. Kaplansky’s direct-finiteness conjecture in characteristic two. The Mezard-Parisi formula for diluted spin glasses. Spontaneous magnetization in the quantum Heisenberg ferromagnet. Isomorphism of free group factors. The three-dimensional relativistic Vlasov-Maxwell system.

Two of those ten are physics in mathematical clothing. Spin glasses and the quantum Heisenberg ferromagnet are statistical mechanics problems and the Vlasov-Maxwell system is plasma physics. That matches a Japanese post in our scan yesterday noticing the release had more physics in it than the English coverage mentioned.

Neither the Hodge result nor either zeta function region is among the ten. The reasoning summaries cover work from the standard pipeline and the two exceptions to that pipeline, which are the two that made the headlines, aren’t included.

852 Forks In A Day Is The Part That Resolves This

Normally a story like this sits unresolved for months while reviewers work.

Not this one. 852 people forked the repo inside 24 hours, a 9.6% fork ratio and forking a Lean library has one obvious purpose. You pull it down and compile it. The repo even warns you to compile small portions at a time rather than the whole library and flags that Linux’s vm.max_map_count may be too low to build it all.

So within days there’ll be public reports of what compiles and what doesn’t. That’s a completely different timeline from waiting on referees and it’s the real consequence of shipping maths as code rather than as PDFs.

Watch for a specific kind of report when it starts. Not “I compiled it” but “declaration X in file Y failed with this error”. One failed declaration doesn’t invalidate the other 184 and a clean build across all of them doesn’t establish that the formal statements match the English ones. Precision in the bug reports is what’ll make this week useful instead of noisy.

The 560 unformalized ones get no such shortcut. Those run on human time.

What You Should Actually Do

If you’re not a mathematician and almost nobody reading this is, there are exactly two useful moves.

Check Whether The Claim Is One Of The 162

When you see a result from this repo quoted anywhere, check whether it’s in the formalized list. Open lean/formalization.yaml and search the title. If it’s there, a machine has checked a formal statement and you can go look at the named declaration yourself. If it isn’t, you’re reading an unrefereed preprint written by a model, which is interesting and not the same thing.

Ignore Conjecture Names For A Week

The second move is to discount conjecture names in headlines entirely for a few days. The Hodge Conjecture is one of the Millennium Prize problems and “proof of the Hodge Conjecture for CM abelian varieties” is a restricted case, not the prize. Those two things read identically in a tweet and differ enormously in substance. The same trap sits under the zeta function result, where the repo itself lists two different zero-free regions and only the weaker one has a Lean proof.

Compiling One Declaration Yourself

If you want to check something firsthand, the barrier is lower than you’d think. Install Lean and lake, clone the repo, pick one declaration from status.main_results, build only that portion. You won’t understand the mathematics. You will find out whether it compiles and right now that’s the question with an answer.

This is also the third version of the same story in six months, so pattern recognition helps. When Donald Knuth went through Claude’s maths by hand, the verdict was that the output looked right until a specialist read it closely. When GPT-5.4 outscored human experts, the score was real and the benchmark turned out to be the thing worth arguing about. Same shape again. The artifact is real, the number is real and the open question is always what the number measures. Formalization is the first version of this story that hands you a way to check rather than a reason to trust.

One more thing worth saying plainly. Nobody involved here is lying to you. OpenAI’s README is careful. The Lean catalogue publishes its own review status as unchecked, which is a weirdly honest thing to ship. The distortion happened entirely in the retelling, where “162 of 722 carry machine-checked proofs, review pending” compresses badly into a post that wants to be exciting. That’s a media problem rather than a maths problem and it’ll repeat with the next release.

For the rest of this week’s local model stack, our Strata piece covers running a 125B model on a gaming PC. Fresh Commits 05 covers the decision model cluster eating the new repo list.

/separator

The Part Worth Keeping

722 manuscripts. 162 Lean proofs. Review status: unchecked.

OpenAI published all three of those facts and the third one is in a YAML file almost nobody opened. The gap between what the repo says about itself and what travelled on X isn’t a scandal, it’s just what happens when the careful sentence is three clicks behind the exciting one.

The interesting shift is that this is checkable at all. A model wrote 722 papers, an agent formalized 162 of them and 852 strangers pulled the library down on day one to find out whether it builds. Maths shipped as code gets audited in days.

Whether any of it is new mathematics, we’ll know soon. Whether the headlines were accurate, we already do.

Charts and Blocks

722 Manuscripts, 162 Lean Proofs

Where The Formalized Work Landed