The dependency was in the prose

A README in OpenAI's new mathematics repository carries a displayed equation that no announcement would:

The file is a withdrawal notice. In a manuscript claiming the algebraicity of Weil classes on split abelian eightfolds, every reverse stabilization trace had been assigned sign \(+1\), so inserting \(m\) of them was supposed to drive a signed double-point count to zero. Accounting for the opposite source orientations of the two branches of the standard cusp gives each trace sign \(-1\) instead, and the count lands at \(-2m\). The Eliashberg-Murphy cancellation theorem invoked at that step needs the count to be zero, so its hypothesis is not met and, in the notice's words, "the subsequent oriented-surgery and embedded-brane construction is therefore unsupported".

Two other papers went with it. One of them says why: "The proof relies on an adaptation of the flawed stabilization-trace construction." All three were withdrawn on 6 October, the day the collection was published.

What OpenAI published that day is large and, by the standards of this genre, unusually honest. The catalogue holds 719 manuscripts organised into 372 families, Apache-2.0 licensed, produced by an unreleased internal model that was posed roughly 4,000 problems and averaged about three hours of ChatGPT Pro thinking compute per result. Alongside the PDFs sits a Lean library of some 122,000 files, 416 machine-checkable verification jobs, and the figure everyone has quoted: "The repository has ~42% top-line results formalized."

That percentage is the weakest artefact in the release, and not because anyone inflated it. It is weak because this corpus's correctness is a property of chains of papers, and the repository records no chains. The verification machinery is excellent at the thing it checks and silent on the thing the withdrawals demonstrate.

What the machine actually certifies

In Lean, a mathematical statement is a type and a proof is a term of that type, so checking a proof is not reading it. A small kernel asks whether this term inhabits that type. Whatever it accepts, follows.

That leaves one way to cheat that has nothing to do with faulty logic. State the theorem in your paper, then in the Lean file prove something adjacent and weaker that happens to compile. The kernel approves it, because the kernel is not comparing anything to anything.

The release closes that hole with a tool called Comparator, and this is the best engineering in it. Every result gets two Lean files. The challenge module states the theorem and ends in sorry, a deliberate hole where the proof would be. The solution module proves it for real. Comparator then builds both inside a sandbox, exports both environments, and confirms that every declaration appearing in the statement matches between them, that the solution's proofs depend on no axiom outside an allowlist, and that the whole thing replays through the kernel. Across all 416 configs in the repository the allowlist is identical and minimal: propext, Quot.sound, Classical.choice, the three standard axioms of Lean's library and nothing else.

One challenge file shows how much work this does. TamingCompatibility.lean, for Donaldson's tamed-to-compatible conjecture, imports no convenient definition of "compatible". It writes out from scratch what a two-form on a four-manifold is, what makes one smooth, closed and non-degenerate, what an almost-complex structure is, what it means for a form to tame one and to be invariant under it, and only then states the theorem: if some symplectic form tames \(J\), then some symplectic form is compatible with \(J\). A reader who knows the mathematics can audit that statement line by line without reading any of the proof. That is the point of the design.

So the chain of certification has three links. The kernel establishes that the proof follows. Comparator establishes that the proof proves the challenge statement. And something has to establish that the challenge statement is the theorem in the paper. The first two links are machines. The third is a person, and Comparator's own documentation is explicit about it: the tool takes "a challenge file, which you trust". Trust, here, is not a property the software supplies. It is supplied by whoever wrote the challenge.

In this release, the party claiming the proofs wrote the challenges too.

The repository says so, in a field nobody read

OpenAI did not hide this. It filled in formalization.yaml, a self-reporting standard from the Mathlib Initiative whose stated purpose is to capture "the things that aren't mechanically obvious from the source tree: provenance, intent, process, and how faithfully the formalization tracks its source". The standard's one required judgement field is review.status, whose vocabulary runs unchecked | agent-reviewed | self-assessed | peer-reviewed | author-verified.

OpenAI's catalogue says unchecked.

That is the most informative line in the release and I have not seen it quoted anywhere. Three further fields of the same standard are left out entirely: fidelity.divergences, for "places the formalization deviates from sources: generalizations, weakened hypotheses, renamed lemmas"; alignment, for how source statements map to formal declarations, with a per-statement vocabulary that includes the values literature-dependency and not-formalized; and, on each of the 200 main results the catalogue lists, literature_dependencies, defined by the schema as "results this result relies on but does not prove, assumed from the literature". Every one of those 200 entries carries exactly three keys: a config, a declaration, a filename. No dependencies, no axiom list, no sorry count.

Some of that work does exist, in prose. The lean/docs/ directory holds 242 scope notes, one per family, and they are candid in a way the percentage is not. The note for the irrationality exponent of \(\pi\) states the formalised result and then adds that "the paper's convergence consequence for the Flint-Hills series is outside this selected statement". The Mahler note says the symmetric conjecture and its equality cases are formalised and that "the nonsymmetric Mahler conjecture and the functional inequalities are not included". This is exactly the right disclosure. It is also 242 paragraphs of English, one family at a time, and a single number is what travels.

Try to reconstruct that number and the problem becomes concrete. The 7 October history entry gives it as "300 / 719 = ~42%". The machine-readable catalogue, at that same commit, lists 173 papers with a formalised main result and 200 result entries pointing at 189 distinct Comparator configs; 173 of 719 is 24%. Counting every paper that merely sits in a family where something was formalised gets to 273, still not 300. Meanwhile the tree holds 416 Comparator challenges, of which the catalogue names 189 and the directory's README accounts for 5 more as deliberate checks of supporting results rather than main theorems. The catalogue describes its own scope as "Partial progress", which is honest and leaves the headline figure derived from nothing a reader can see.

Then there is what a stale pointer looks like. On 6 October "Taming implies compatibility on four-manifolds" was revised to restrict a cone-sum equality to the case \(h_J^- = b_2^+ - 1\) and to add a four-torus example of strict inclusion. The manuscript map points at that revision; the formalization catalogue and the family's scope note still point at the superseded 23 September edition. The Lean statement looks untouched by the narrowing, since it proves the tamed-to-compatible conjecture and says nothing about cones. Nothing in the repository asserts that, and the only way to know is to read both PDFs and the Lean file yourself.

The strongest case for the release

This is the most inspectable publication of machine-generated mathematics anyone has produced. It ships the sources under a permissive licence, adopts a third party's self-reporting standard rather than inventing a flattering one, documents per-family scope limits, pins its axiom allowlist to the minimum, logs corrections with the offending equation, and archives pre-withdrawal PDFs at a named commit. Compared with a press release announcing that conjectures have fallen, this is a gift, and the withdrawal came within a day.

Every document cited above was published either by OpenAI or by the authors of the standard it adopted, because nothing else about this release was reachable from here; none of the 719 manuscripts has been peer-reviewed, and nothing here is an independent reading of the mathematics.

That case is true, and all of it is why the gap matters. A release at this standard sets an expectation that its artefacts describe themselves. The three withdrawn papers appear nowhere in the formalization catalogue, so the error was found the old way, by a person reading prose, and it propagated the old way, through an argument that cited another argument. Two of the three withdrawals were dependency failures, visible only to someone who read the manuscripts. The repository went on to revise 14 more and update 13 others purely so they cite the corrected editions: 27 manuscripts carry version notes four days after publication. A percentage cannot see any of that, and the schema has a field for all of it.

What to do with a number like 42%

When something is described as machine-verified, ask three questions in order. What statement was checked? Who decided that statement is the theorem? What does the checked result assume that was not checked? For this corpus, Comparator answers the first very well, the catalogue answers the second with the word unchecked, and the third has no field filled in at all.

The useful unit here is therefore the family, not the percentage. Before believing any headline from this release, open lean/docs/<family>.md and read what the scope note excludes. It is the difference between "the Mahler conjecture is proved" and what was certified.

The deeper lesson is about where the bottleneck in AI mathematics has moved. It is no longer finding proofs; 4,000 problems in and the model produced 372 families of results worth publishing. It is agreeing on statements. Autoformalisation, the translation of a prose theorem into a formal one, is the step that now carries all the residual risk, and it is the step that does not scale, because every honest version of it ends with a human being reading two documents side by side and judging them the same.

The withdrawal notice closes with a sentence a mathematician would write and a marketing department never would: "This withdrawal concerns the proof; it does not assert that the mathematical statement is false." That distinction is the whole of the thing. A kernel can tell you an argument follows. Only a reader can tell you what it was an argument for. OpenAI shipped 122,000 Lean files and 242 paragraphs of English, and it is the 242 paragraphs that nobody has figured out how to automate.