On the sixth of October OpenAI put 719 mathematics manuscripts on GitHub. Three days later the Association for Human Mathematics called for a boycott, on the grounds, in their words, that "releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power." The replies split along the line you would expect. One side says nobody asked for this. The other side asks whether a human who had done the same thing would be getting the same reception.
Underneath both positions sits a single quantity, and it is a number, not an opinion: how many hours of a competent person's attention it will take to find out whether any of this is true.
Nobody in the argument has mentioned that the repository answers most of that question itself.
The directory nobody cited
Next to the manuscripts there is a Lean library. Lean is a proof assistant: you write a theorem and its proof in a language a computer can check, and the computer either accepts it or it does not. A result that has been formalised this way costs a reader almost nothing to verify. You install the toolchain, you run the build, and the machine tells you. The repository even ships the harness for doing that, a tool called Comparator, with one configuration file per claim.
So the real question about this release is not whether an AI wrote it. It is how much of it comes with a file a computer can check, and how much is prose that a person has to sit down with.
I counted.
One result, several papers
The first thing to get straight is what you are counting, because the repository counts two different things and the published percentage mixes them.
719 is the number of manuscripts. The number of results is 372. OpenAI calls these result families, and defines a family as a principal result together with its companion arguments, its consequences, or alternative proofs of the same thing. One family averages just under two papers; the largest has fourteen. So when somebody says seven hundred proofs, the honest figure for distinct advances is 372, and the repository says so on the first line of its own contents page.
Of those 372 results, 242 have Lean work attached. 130 do not.
That is the number. Thirty-five per cent of the results in this release have no machine-checkable artifact of any kind, and for those the only route to confidence is a mathematician reading a PDF. The other sixty-five per cent have at least one of the 416 Comparator challenges, and you can run those yourself this afternoon.
Be careful which way each figure errs. The 130 is exact: those families have no Lean file, no scope note, nothing. The 65.1 per cent is an upper bound, and not a tight one. Having Lean work attached is not the same as having your headline theorem proved, and the repository is candid about the difference. 42 of the 242 scope notes state in prose that something is outside the formalisation. Seven of the 416 challenge files are named with the suffix Support, which the Comparator readme explains means they "verify supporting results, not the corresponding papers' main theorems". The true main-result coverage sits below 65.1 per cent by some amount I cannot pin down from the files, and I would rather say that than pick a number.
Where 42 per cent comes from
The repository's own headline, added on the seventh of October, reads: "This brings the total percentage of top-line results formalized to 300 / 719 = ~42%."
The numerator is described as top-line results. The denominator is manuscripts. By the repository's own definition a family has one top-line result, so the matching denominator is 372. Divide 300 by 372 and you get eighty per cent, which is higher than anything I can support. Divide the number of results that have any Lean at all by 372 and you get 65.1, which I can. Either way the published figure is not comparable to either, because its two halves count different objects.
The 300 is harder to place. I went looking for it in every machine-readable file in the repository and it is in none of them. formalization.yaml, the file whose first comment calls it a "Catalog of papers with a formalized main result", names 173 papers and 200 declarations. There are 416 Comparator configurations on disk. 242 families have a scope note. No count is 300.
That file also tells you not to lean on it. Its scope field says "Partial progress." Its review status says unchecked. Its automation method says agent. OpenAI is being straight about the thing: the index is incomplete and says so, which means the headline percentage cannot be reconstructed from it and is not meant to be.
The parts that are better than the argument allows
Two things in this repository deserve to be said out loud by somebody who is not on either team.
The scope notes are real documentation. Every one of the 242 families with Lean work has a file describing exactly what got formalised, and 42 of them say in plain prose that something did not. The note for the quasi-Riemann hypothesis tells you the principal-character poles are excluded, that the constant in the Landau–Siegel bound has no explicit value, and that the paper's later applications are not covered. That is a person writing down the limits of their own claim, and it is more than most preprints do.
And the thing came back bleeding within a day. On the seventh of October, one day after release, three manuscripts were withdrawn because a sign error in a stabilisation-trace argument invalidated a construction that two other papers depended on. Fourteen more were revised. The withdrawal notice names the error and links the archived version. Every directory in the repository carries its edition date, so the superseded copies are still sitting there; I can account for all 749 directories as 719 current, 27 superseded, 3 withdrawn, with nothing left over.
A sign error killing three papers in twenty-four hours is the boycott's argument and the repository's defence at the same time. It is exactly the failure mode you would predict from unverified volume. It was also caught, named and published faster than any journal has ever managed.
The category that did not exist
I should say where my own count went wrong, because it went wrong in the direction that would have made a better story.
My first pass used formalization.yaml as the list of formalised main results and compared it against the scope notes. That produced a third group: 107 families with Lean work but no main result in the index. A hundred and seven papers with proofs of something other than what they claim. It is a good headline and it is false. I went and read six of those scope notes and every one begins "The formalization proves" followed by the family's headline claim. Kadison's similarity problem. The triangular lattice minimising Riesz energy. The joint Dickman law. The index is partial, it says it is partial, and I had treated it as complete.
The category was a hole in my instrument. It took reading six files in prose to find, after the arithmetic had been clean for an hour.
Three other rulers lied on the way. A link-matching rule anchored on a closing bracket silently truncated the one directory with a bracket in its name and gave me 718 manuscripts against a stated 719, so the off-by-one I was briefly suspicious of was mine. The same rule crashed on the only row in all 719 that carries a note after its link. A field matcher that forgot a list dash reported zero configuration files in a document containing two hundred of them.
None of that is unusual. It is what measuring is.
What the fight is actually over
Strip out the question of who wrote it and the release is 372 claims, of which 242 arrive with something a machine can check and 130 arrive as prose.
That second number is the one to argue about. 130 results is an enormous amount of unpaid reading, and it lands on referees who did not ask for it and are not being funded to do it. The boycott is not wrong that this is a cost transfer. Where it goes quiet is on the other 242, because "run the checker" is a worse grievance than "read seven hundred papers," and 65 per cent of the thing can in fact be checked by running the checker.
The symmetrical blind spot sits on the other side. If a formalisation makes a result cheap to verify, then the 130 without one are not yet results in the sense the field means. They are drafts with a strong prior. The repository agrees: "Some of the unformalized results could have issues."
A proof is a social object. Its job is to make somebody else certain, and the work of making them certain is work that someone has to do. For 242 of these a computer will do it. For 130 a person will, or nobody will, and the second outcome is the one worth being angry about.
Every figure above comes from four files in the repository and is reproducible from them. The per-family table is published as a free CC0 dataset at /writing/openai_math_lean.json, along with the four instrument errors named in full. The generator refuses to emit anything if any of its nine validation gates fails; the gates were each sabotaged deliberately and each one fired.