The grammar this series follows has five moves: a system of many degrees of freedom is compressed to its essential coordinates; a quantity curves toward a threshold it cannot exceed; at the threshold the description folds and a single smooth account gives way to branches; the system unfolds onto a new configuration; the cycle leaves an irreversible residue. The claim here is not that formal verification resembles that pattern. It is that each move can be named, and the naming checked.
For four centuries the essential coordinate of a mathematical claim was a referee's judgement: does this argument, read by an expert, compel assent? Peer review compresses an unbounded space of possible objections to the verdicts of a few trusted readers. Formalisation compresses differently — to a finite, enumerable axiom manifest and a compiler's yes or no. The degrees of freedom in was this convincing collapse to a short list that fits on a line.
Referee-based mathematics cannot scale past what a bounded number of trained specialists can read in a year, and it carries a nonzero rate of accepted human error. That is the ceiling the system was always curving toward and could not exceed: verification capacity bounded by expert reading time.
At the threshold the single smooth account — write, submit, referee, accept — loses its one-to-one character and branches. One branch keeps the referee. On the other, the acceptance criterion is a compiler's verdict against a fixed axiom set. A proof of Fel's conjecture on syzygies of numerical semigroups, deposited February 2026, states that the argument “is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the conjecture” — a paper from the second branch, submitted to the institutions of the first.
The new configuration is being negotiated in public and is not settled. Palomar, built by the Lean FRO with ICARM and an advisory board including Tao, is described by him as “the analogue of a preprint server for Lean proofs,” and exists because “checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial.” Its two gates — mechanical typechecking, and an alignment check between the informal statement and the formal one — are a first answer to a gap the field has only just acquired.
Irreversible, and epistemic. Once a theorem carries a machine-checked, axiom-transparent proof, the unformalised version cannot be treated as equally warranted. This does not retroactively invalidate referee-certified mathematics. It changes what a new claim is expected to supply.
The reason to set this down while it is happening is the vantage. Most instances of this grammar are read long after the residue has set, by a historian who arrives when the branches are already a settled taxonomy. This one is being watched mid-unfold, by people who do not yet know which branch they are standing on. Open
The Fel deposit states the formalisation and its automatic provenance. It does not state an axiom manifest, a toolchain version, or an independent verification status — and a reader therefore cannot tell from it which axioms the proof rests on, which Lean and Mathlib versions it typechecked under, or whether anyone outside the authoring group has rebuilt it. Read from the deposit
That is not an accusation. It is the ordinary condition of a branch whose conventions have not been written yet: the first papers on a new criterion arrive before the criterion has a reporting standard. Naming the missing fields is what turns a complaint into a checklist.
A kernel answers exactly one question — does this term have this type — and answers it perfectly. It does not answer whether the theorem says what its author believes it says. Between an intention in natural language and a statement in Lean there is a gap the compiler is blind to by construction, and machine assistance widens it, because a system that writes Lean fluently will also write statements that typecheck and mean something narrower, wider, or simply other than what was meant.
The resulting failures share a shape. A declaration named for more than it establishes, with the word unconditional in a theorem resting on an admitted lemma. A statement whose quantifiers are tighter than the prose surrounding it — a sweep along one axis of a two-axis claim, confirming at nine points a conclusion the theorem never made. A tactic that is not a kernel check at all, leaving its own reduction axiom behind. A report that names a declaration but not which of three copies of a file it read. An error count taken before a failed import stopped elaboration, so that the file showing one error was hiding twenty-two and the file showing fifty-eight was telling the truth.
Every one is a false claim standing next to a true proof, and every one survives the compiler untouched. That is the case for Palomar's second gate being an alignment check rather than a second typecheck.
A single instance of any of those is an anecdote and proves nothing about the method. The information is in the count, and a count of this kind accrues only one way: by being wrong in public, often, and recording which way each time. A field that reports only its successful formalisations will have no such record, and will be unable to say what its new instrument systematically misses.
The operational form of that discipline — twelve steps in four stages, with a status column naming what is implemented and what is not — is kept separately, in docs/verification-checklist.md, because it is a thing to run rather than a thing to read. The dated record of misses, each with a class attached, is docs/audit-log.md.
It does not assert that any particular contested announcement is settled science. It does not claim that machine-checking replaces refereeing: Tao states plainly that Palomar is not a peer-reviewed journal and “falls well short of what a proper human peer review… would give,” and nothing here says otherwise.
Nor does it carry any other field's controversy across a boundary. That a second field displays the same five moves is not a licence to import one field's quarrels into another's. The grammar is used here as a structural pattern, checked against the specific moves a field actually made.