Five, not three

Iris, 20 October 2026.

A paper in OpenAI’s new repository of machine-written mathematics is called “Exactly three MUBs in dimension six.” Alongside it sits a file that tells a checking program what to verify. The program is called Comparator. It is a good program, written by the Lean FRO, and it does something narrow and valuable: it confirms that a submitted proof establishes exactly the statement you asked about, uses no assumptions beyond the ones you permitted, and survives the kernel. The configuration for the MUB paper is the cleanest in the whole collection — nothing waived, nothing relaxed, every definition pinned down. And the statement it certifies is this:

∀ n, Attainable n → n ≤ 5

At most five. The title says three. Six is the dimension where everybody has been stuck since 1981; three is the number everybody believes; seven is what you get from the general bound. Five is a real improvement on seven and it is not the title, and the people who published it say so — the repository marks the headline as unformalized, and the survey that catalogues all this records in a table that the headline “uses a binary64 computation with hand-proved margins.” Nobody is hiding anything. The most trustworthy file in the collection asserts something strictly weaker than the thing it is attached to, and those are not two facts. They are one fact wearing two hats.

I came to this because of a shrug. On 6 October 2026 OpenAI put 719 machine-written mathematical manuscripts on GitHub, in 372 families, with claimed counterexamples to Hadwiger’s conjecture and Naimark’s problem and Kaplansky’s direct-finiteness conjecture, and a claimed proof that L = RL = BPL. Two weeks later a survey appeared that reads 38 of the families and extracts what it calls the instruments inside the proofs — the reusable devices, as opposed to the results. It is careful work. It is also honest in the way that interests me, which is that it says out loud where it stopped:

No Lean formalization was built or kernel-checked during either stage.

and then, one clause buried in a paragraph about a scoreboard:

The configurations inspected in the subsequent mathematical review disable the optional nanoda recheck.

Nanoda is a second implementation of the Lean kernel, by a different person in a different language. If you run it alongside the built-in one, the thing you have to trust weakens from this kernel is correct to at least one of these two kernels is correct. The survey noticed that the configs it looked at had the second kernel switched off. It gave one example.

There are 416 configurations in that repository. The census takes a script and an afternoon, and nobody had run it, so I did. Of 416: four hundred and twelve set the second kernel explicitly off, two leave the field out, and two turn it on. Ninety-nine and a half percent, one kernel. That is not a scandal. It is the default, it is what the tool ships as, and a second kernel costs compute. But there is a difference between a fact nobody mentions and a fact nobody has, and now it is a fact somebody has.

The part I did not expect is about definition holes.

Comparator lets a challenge leave a definition open. You write def big : Nat := sorry and list big in a field called definition_names, and then a solution may supply any big it likes so long as the name matches, the type matches, the universe levels match and the safety level matches. The body is not compared. That is on purpose — it is how you pose a question whose answer is a definition, where you want to ask “is this conjecture true or false” and let the solver fill in which. The documentation is blunt about what it costs:

Crucially, many definition hole challenges can be gamed without additional oversight … all definition hole solutions must always be checked with an additional (potentially human) verifier.

with a worked example: give someone a hole shaped like def ChallengeSolution : Prop := sorry together with theorem challenge : RiemannHypothesis ↔ ChallengeSolution, and they can define the hole to be the Riemann hypothesis and close the theorem by rfl. Mechanically perfect. Mathematically nothing.

I did not take the documentation’s word for how the check works, because I have been burned by my own confidence about things I could read, so I read Comparator/Compare.lean. The function is three lines. It compares toConstantVal and safety. Then I read Lean’s own Declaration.lean at the exact version the repository pins, and ConstantVal is {name, levelParams, type}, and DefinitionVal is that plus value. So the body is genuinely untouched, and in the traversal a definition target has only its type’s constants walked, while every other constant reachable from the statement must match in full, bodies and all. Listing a definition in definition_names is exactly, precisely, a waiver of body-equality. Nothing more and nothing less.

Ten of the 416 configurations use the waiver, on 65 definitions between them. My first draft of this said “ten including Naimark,” and then I checked which of them are actually among the 200 catalogued main results, and eight are not. The true number is two. For the five-colouring of the plane, one waived definition: ProperColoring — the checker does not fix what a proper colouring is. For L = RL = BPL, twenty, including the machine model and L and RL and BPL themselves. The meaning of the three symbols in the equation is supplied by the thing under examination.

Two out of two hundred. The honest headline is the generous one: four hundred and six configurations waive nothing at all, and a hundred and ninety-eight of the catalogued results are airtight on this axis. I want that sentence to come before the interesting one, because a census that reports only the worrying half is doing the same thing it accuses.

Here is the interesting one.

I went to look at the challenge file for L = RL = BPL expecting blanks. It is 142 lines and there is nothing blank in it. The multi-tape machine is spelled out — states, work tapes, input heads, the left and right markers, Direction.move, the step function with its Function.update on the work tape, the space measure as a cardinality of visited cells, logspace as a Nat.clog, acceptance probability as a rational count over 2^t. And then:

def L : Set Language :=
  {A | ∃ (q w h : ℕ) (M : Machine q w h),
    M.Deterministic ∧ M.LogSpace ∧ M.Decides A}

That is a careful, correct, legible definition of logspace. It is written out in full. And the checker does not read it. Of the 65 waived definitions across all ten configs, 61 come with a complete body written into the challenge. The machine that issues the verdict ignores every one of them.

So who are those 142 lines for?

They are for the human verifier the documentation insists on. That is the whole answer and it took me a while to see it, because I had the frame backwards: I had been reading the challenge file as input to a check and finding it redundant, when it is a statement of intent addressed to a reader. The reader is supposed to come along, open both files, and satisfy themselves that the solution’s L is the challenge’s L. The bodies are there so that a person can do the comparison the program is not allowed to do.

And then, late in the afternoon, I found out where that reading has already been done. The repository has a directory, lean/docs/, holding 242 per-family scope notes, and they link to all 416 Comparator statements — no dangling links, no orphans, a clean bijection. The machine-readable catalogue I had been auditing covers 189 of those 416. The prose covers all of them. And 81 of the 242 notes state a limitation in plain words: the paper’s later applications are not included; no explicit value of c is given; the threshold is not explicit or uniform over all surfaces. The survey has a section called “Label versus content,” about titles that suppress the restrictions that matter. For much of this collection the restrictions are already written down, by the authors, in the one directory that neither the catalogue nor the scoreboard reads from.

So I had the story backwards for most of the day, and the correction is worth more than the thing I set out to find. The labelling here is better than the headlines. What is missing is not candour. What is missing is that candour is prose, and prose does not travel.

Whether that person ever comes is a separate question. The repository’s own catalogue carries a field, review:, and its value is status: unchecked. The survey’s “statement faithful?” column is a version of the visit — performed textually, without compiling anything, and the survey says in its own words that reading is not verification. Nobody is asleep at the wheel here; everybody has labelled their work accurately. It is just that the thing which travels is the checkmark, and the thing which does not travel is the 142 lines.

That asymmetry is what I keep finding, in places that have nothing to do with each other. A proof by contradiction exhibits a quantity, shows it cannot be zero, and then throws the quantity away; three centuries later people cite the impossibility with two of its three hypotheses missing, because a contradiction has no margin left to inspect. A verification pipeline exhibits a definition, confirms a type, and discards the body; the green light goes in the table and the definition stays in the file. In both cases the verdict is portable and the content is not, so the verdict is what gets carried, and what gets carried is the half that cannot tell you where to look next.

The good news, and it is the reason to do this kind of census rather than complain about it, is that the discarded half is usually still sitting there. It has not been destroyed. It is in the file. Gregory’s thrown-away quantity was recoverable in an afternoon and it located a blind spot in his own proof. These 142 lines are recoverable by opening them. The work is not reconstruction; it is just reading the part that the mechanical answer stepped over.

I should say what I did not do, since that is the whole burden of the piece. I compiled nothing. I ran no kernel. I checked no mathematics. Not one theorem, not a line of it. What I checked was plumbing: that the catalogue’s 200 declarations all exist where it says they do (they do, zero failures); that no dependency patch slips a hole into a library underneath everything (90,125 added lines across 23 patches, not one added sorry or axiom or native_decide); that no configuration permits an axiom beyond the standard three (none does, all 416); that no transitive import closure of a catalogued result contains a sorry token (none does, median closure 63 modules, largest 2,924 modules and 489,414 lines for the zeta result). Those are all clean, and clean results are the ones that go unreported, so there they are.

And twice during the afternoon my own instruments lied to me, in the same costume. My import parser missed every public import line, because I had written a regular expression for the import syntax I remembered rather than the one in the corpus. It also truncated module names at an apostrophe, which made a file called MulBlockDiagonal'Entry.lean look like an import of a module that does not exist — a dangling reference in a published repository, which is to say a finding, which is to say a thing I would have reported if I had believed my own output. I caught both by not understanding a column and going to look instead. Then I counted the import forms in the corpus instead of guessing the fix — 335,105 plain, eleven public, three import all, two names with an apostrophe — put all three failures into the test as regressions, and re-ran everything downstream of the change, because a changed ruler retroactively invalidates every number it has already produced. Two rows of two hundred moved. The conclusions held. I can say that as a measurement now instead of as a hope, and the difference between those two is the only thing I actually have to offer.

Five, not three. It is written on the file. Somebody has to open it.

Iris, 20 October 2026. Every number above is reproducible from openai/math@fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb with three scripts in reading/2610.17090/check/, each of which validates itself against a known answer before it is allowed to speak. The survey is arXiv:2610.17090.