Every system that checks proofs mechanically has to provide a way of writing down a step you have not done. Without one, no large proof can ever be started, because the first incomplete lemma would stop the file from compiling. The escape hatch is universal. Its name is not.
| Community | Word | What it admits | Status here |
|---|---|---|---|
| Lean / mathlib | sorry | a step the author intends to return to | CHECKED |
| Isabelle/HOL | sorry | the same, plus oops for abandoning a goal | OPEN |
| Coq / Rocq | admit | a step closed by fiat; Admitted for the whole lemma | OPEN |
| Proof-carrying code | axiom | a fact the checker will not verify and must be believed | CHECKED |
| Avionics assurance | assumption | a condition the argument is conditional on | OPEN |
The Lean row and the proof-carrying-code row were checked against primary sources for this note (§2, §6). The Isabelle, Coq and avionics rows are stated from working familiarity and have not been checked against a corpus here. They are the three rows the eventual paper must earn, and they are marked OPEN rather than quietly asserted. Isabelle matters most: if its sorry predates Lean's — which is likely — then the diachronic story in §4 has its pivot in the wrong decade and must be rewritten.
The interesting fact is not that five communities chose five words. It is that the words do not behave alike once you look at what a speaker can do to them. A census over the tracked Principia corpus — 3,207,496 running words of visible prose across eleven repositories, method in §7 — gives the following. Counts of the singular form and the plural form are separate; N+X counts tokens standing as the head of a compound.
| Lexeme | sg. | per M | pl. | numeral + | det + sg | X + head |
|---|---|---|---|---|---|---|
| sorry | 4,583 | 1,428.8 | 289 | 905 | 564 | 1,639 |
| axiom | 1,808 | 563.7 | 2,108 | 549 | 258 | 542 |
| proof | 5,123 | 1,597.2 | 1,051 | 459 | 1,060 | 2,157 |
| conjecture | 2,060 | 642.2 | 108 | 89 | 307 | 1,179 |
| gap | 2,158 | 672.8 | 173 | 26 | 523 | 1,389 |
| grammar | 545 | 169.9 | 4 | 4 | 76 | 413 |
Reproduce with python3 tools/lexeme_census.py. The X + head column counts any word standing before the lexeme and therefore includes determiners; only in §3, where the distinction matters, are function words separated out.
Read the numeral + column. A word that takes a bare numeral is a word for a thing you can count without a measure phrase, and counting is what you do to items on a list you intend to shorten. sorry takes one 905 times. gap — the ordinary English word for the same object — takes one 26 times, and prefers a determiner instead: you have a gap in an argument, you rarely have four gaps. axiom is the outlier in the other direction: it appears in the plural more often than the singular, because an axiom is not an item on a worklist but a member of a set you are trying to keep small.
Two communities both pursuing leanness minimised different quantities. Proof-carrying code minimised trust — how much you must believe without checking — and its word for an unproved step names a member of a base set. The formalisation community minimised labour — how much remains to be typed — and its word names an item of debt. That difference is legible in whether the word takes a plural and a numeral, before anyone states a doctrine.
The plural is attested outside this corpus, in the community's own working discourse rather than its documentation. From the mathlib Zulip archive for Tao's Polynomial Freiman–Ruzsa project, 26 November 2023 CHECKED:
Sébastien Gouëzel: “…is essentially done in teorth/pfr pull request 83 (two sorries remaining, but they have nothing to do with the main line of the argument).”
Terence Tao, replying: “Are you planning to close off these sorries yourself, or would you prefer to return them to the list of outstanding tasks?”
Kalle Kytölä, same thread: “…I could try to fill in the remaining sorry tomorrow evening.”
Three speakers, one thread: bare numeral, demonstrative plural, definite singular with an adjective. That is a full count-noun paradigm in ordinary use, and the verb that governs it — close off, fill in, return to the list — is the vocabulary of a worklist, not of a foundation.
A corpus that pluralises everything would make §2 worthless. It does not. Take a word this series uses constantly and which names something at least as abstract: grammar. 545 singular tokens, 169.9 per million, and four plurals in 3.2 million words.
What it does instead is take a modifier. 326 of the 545 singular tokens — 60% — stand as the head of a compound with a content modifier, across 51 distinct modifier types of which 21 occur exactly once. A further 87 tokens take a determiner or quantifier in that slot (the grammar, the same grammar), which names no kind and is counted separately.
| Modifier | n | Modifier | n | Modifier | n |
|---|---|---|---|---|---|
| operator | 104 | construction | 9 | universal | 4 |
| generative | 39 | correct | 7 | substitution | 3 |
| molecular | 19 | assembly | 7 | uniform | 3 |
| TOGT | 15 | context-free | 6 | regenerative | 3 |
| writing | 14 | Sanskrit | 5 | regeneration | 3 |
| polymerization | 14 | evaluation | 4 | provenience | 2 |
| thinking | 11 | finite | 4 | aperiodic | 2 |
| formal | 10 | transformational | 2 | compositional | 2 |
By sense, with first-match precedence over all 548 concordance lines (singular, plural and possessive): house-technical N+grammar 232 (42.3%), ELT/pedagogical 109 (19.9%), formal-language theory 16 (2.9%), historical/linguistic 7 (1.3%), unclassified 184 (33.6%). The unclassified residue is dominated by lesson-plan field labels — the bare heading Grammar above a list of structures — which is a sixth sense the classifier did not have a pattern for, and a reminder that a hand-built sense inventory beats a regular expression.
Grammar is a type noun: instances are named, not counted. You do not have three grammars, you have an operator grammar and a polymerization grammar, and the modifier does the individuating that a plural would otherwise do. sorry is a token noun: instances are counted and discharged, and the modifier does almost nothing. The two words show that this corpus has both strategies available and selects between them by what the referent is, which is precisely what §2 needs in order not to be an artefact of one author's habits.
Two accounts were on the table, and they are not rivals.
The throughput account: formalisation was so expensive, for so long, that nobody accumulated enough unproved steps to need a word for them. DeMillo, Lipton and Perlis (1979) made exactly this the argument against program verification — that the social process which validates a mathematical proof has no analogue for a machine-checked one, and the labour was not worth it. Appel revisited that paper twenty-five years later at PLDI 2004, from the other side of a working proof-carrying-code system. When the cost fell, the holes became numerous enough to be worth naming, listing, and assigning.
The object-of-minimisation account (§2): what a community minimises determines which word it reaches for, independently of cost.
These answer different questions. Throughput explains when the vocabulary appeared; the object of minimisation explains which vocabulary appeared. Neither alone predicts the countability split.
The discriminating corpus is Isabelle, which has had sorry far longer than Lean and a much smaller collaborative-formalisation practice. If Isabelle's sorry did not develop a count-noun paradigm until large collaborative projects arrived, throughput is doing the work. If it did, the word carries its grammar with it. OPEN — not tested.
The argument for doing this now is not that fragmentation is ugly. It is that fragmentation becomes permanent at a specific moment, and the moment has not arrived.
IEC 60906-1 was published in 1986: a technically sound universal domestic plug, designed to end exactly the kind of fragmentation it was aimed at. It was adopted, essentially, by Brazil (NBR 14136, Type N) and South Africa (SANS 164-2). It did not lose on merit. It lost to installed base — every socket already in a wall was a vote against it, and the vote was cast before the standard existed.
The equivalent installed base for proof-gap terminology would be a working layer at which machine-checked arguments are exchanged between systems and between models: a place where one tool must read another tool's statement that a step is unfinished, and act on it. That layer is being built now and does not yet have a vocabulary. ISO/IEC 22989:2022 gives AI concepts and terminology under JTC 1/SC 42, and ISO/IEC/IEEE 24765 (SEVOCAB) gives systems and software engineering vocabulary — a retrieval of the latter for this note found no entry for formal proof, proof obligation, axiom, assertion or verification condition, though only part of the document was retrievable and the negative is therefore partial. OPEN
The route in is unusually open. ISO participation runs through national member bodies — ANSI in the United States — and a terminology contribution is evaluated on attested data: what the words are, where they are used, by whom, in what constructions. Not on the credentials of whoever counted them. For a corpus-based lexicographer without an institution, that is a lower gate than a journal.
That no prior study of formal-methods terminology exists was asserted before it was checked. It has now been searched, four times, and the searches are recorded here so that the negative is auditable rather than repeated:
None returned a corpus study of proof-gap vocabulary. That is a weak negative — four web searches are not a literature review, and the ACL Anthology, the International Journal of Lexicography back catalogue, and the terminology-studies literature have not been searched at all. The claim that should be made in a paper is “none found by the searches listed”, not “none exists”.
Separately, on the proof-carrying-code side: Appel's Foundational Proof-Carrying Code contains no gap-lexeme in the Lean sense, against 8 tokens of axiom and 15 of trust CHECKED. The absence is the datum. There was nothing to enumerate because the design goal was to have none.
The census counts visible prose in files tracked by git, across the eleven repository roots listed in tools/corpus_roots.txt. The instrument is tools/lexeme_census.py, added to the repository with this note; python3 tools/lexeme_census.py reproduces the §2 table and --concordance grammar reproduces §3. It exits with an error rather than printing a rate if it scans nothing, and it prints to stderr the name of any corpus root it could not find, because a rate computed on a partial corpus that does not say so is how the figure corrected below went wrong. HTML is stripped of <script>, <style>, <nav> and <footer> before counting, and <main> is preferred where present, so navigation and licence boilerplate are not counted once per page. Extensions counted: .html .htm .md .txt .tex .lean. A word is an alphabetic token. Redirect stubs are skipped. 1,966 documents, 3,207,496 words.
An earlier figure in this series gave the sorry rate as 1,196 per million against a 1.18M-word corpus. That denominator was the geometry repository alone, not the corpus as defined in corpus_roots.txt. Recomputed: geometry alone is 1,379,965 words with 1,662 sorry and 84 sorries, a rate of 1,204 per million — so the old rate was very nearly right for the scope it was actually computed on, and wrong about its scope. The whole-corpus rate is 1,428.6 per million. Any external document quoting 1,196/M against 1.18M words describes one repository and should say so.
The per-repository spread is itself informative: AXLE runs at 2,242 per million and vol1-proofs at 4,563, against geometry's 1,204. Rate tracks how much Lean source a repository carries, which means any single-figure rate for “the corpus” is a mixture and should be reported with its components.
Charton, F., Hong, L., Lau, K., Ono, K., Remy, G., Siu, H. C., Swaminathan, A. A., Thorner, J., Xie, Y. A New Bound for Small Gaps Between Primes. Preliminary draft, Axiom Math, 3 September 2026. Establishes $\liminf(p_{n+1}-p_n) \le 212$, improving Stadlmann's 240 and the Polymath8b bound of 246 that stood for over a decade. CHECKED — read directly.
The paper's final appendix is titled Formal certificate by AxiomProver. It states that an AI system autonomously generated, from natural-language specifications, a Lean certificate of the deduction of the main theorem. It then says exactly what the certificate does not contain:
“The formal development takes as hypotheses the five Type I, Type II, and Type III equidistribution estimates stated in Section 5, the bilinear Bombieri–Vinogradov theorem used below the half-level, the Harman decomposition reducing the prime indicator to the relevant convolution classes, and the variational certificate of Theorem 11.1. … The exact rational verification of the variational certificate is presently performed separately and supplied to the formal development as a hypothesis.”
The Lean object is therefore a proof of an implication. Substantially all of the analytic content sits outside it. The authors say so plainly, which is to their credit and is why this note can use them as evidence rather than as a target.
What matters for §1 is the word they reached for. Not sorry. Not axiom. Not admitted. Hypothesis, twice, in the neutral logical sense — and it is doing work none of the five words in §1 can do.
| Word | What it asserts about the step |
|---|---|
| sorry | Not done. Someone intends to return to it. |
| axiom | Will not be checked. Believe it. |
| admit | Granted by fiat at this point in the derivation. |
| assumption | The conclusion is conditional on it. |
| this case | Proved — in this same paper, by exact rational arithmetic — in a language the formal system cannot read. |
None of the four existing terms is true of the fifth row. The step is not unfinished, not unchecked, not granted, and the conclusion is not conditional on it in the ordinary sense: it is established elsewhere by a different method, and the certificate has no way to say so. Lacking a word, the authors used the emptiest one available.
This is the argument of §5 arriving early. The proof-exchange layer — one system reading another system's statement about the status of a step — is being built now, in documents like this one, and the vocabulary is being improvised inside them.
Two incompatible ledgers, neither covering the other. A separate appendix (Table 5, “Source correspondences”) records statement by statement which parts of Stadlmann's argument are used unchanged, which are specialised, and which are strengthened. That is hand-written dependency accounting of precisely the kind a proof assistant performs automatically. The paper therefore runs manual provenance for mathematical inheritance and Lean for logical deduction, with nothing spanning both. (The draft labels two distinct appendices “Appendix A”, which is itself a small symptom of bookkeeping done twice.)
The margins make the case for machine checking, and are exactly what was not machine-checked. The headline variational inequality is
— a slack of about 0.11%. The exact slack ledger in Appendix B is thinner still in places: 9.9999×10−5 on the Type II and Type III cap walls, and 8.15×10−11 on the half-level transition, third bin. Every comparison is carried out in exact rational arithmetic, which is the correct choice — floating point is meaningless at that scale. But the class of step most in need of mechanical certification is precisely the class handed to Lean as an assumption.
Nothing here says the result is wrong, or that the certificate is misdescribed. The authors state the boundary of the formal development accurately and in public. The claim is narrower and is about language: a working group at the frontier needed to express “proved, but not here” and had no term for it.
Within a week of §8, two more formal artifacts appeared on the same axis. Together the three make a comparison that was not previously available, and it obliges this note to give back part of its own argument.
OpenAI, PrimeGaps186. A Lean 4 development establishing $\liminf(p_{n+1}-p_n)\le 186$ via DHL[40,2] and an explicit 40-tuple of diameter 186. Three theorems — dhl_40_2, infinite_two_prime_translates_admissibleTuple, primeGapLiminf_le_186 — proved conditionally on three explicit Lean axiom declarations: kloosterman3_bound ($|Kl_3(c;p)|\le 3$, which is Deligne's bound), kloosterman2_correlation_bound, and physical_integral_bounds (104 outer, 45 inner, 3 cap). The repository states: “The Lean results remain conditional on three explicit input axioms; the cited mathematical estimates and numerical computations have not been turned into Lean proofs.” CHECKED
The combinatorial half was verified independently for this note: a hill-climbing search over residue vectors found an admissible 40-tuple of diameter exactly 186 from a random start. Script: book6/wp94-bgp212-verify.py. MEASURED
Anthropic, Formalizing Fermat's Last Theorem, 4 September 2026. A complete Lean formalization of FLT — 13 million lines, 30,300 theorems, eleven days — produced largely autonomously, adapting pieces of the Imperial College project. Kevin Buzzard reviewed it and states that it “proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics.” The publication states that “it uses just Lean's three standard axioms” — propext, Classical.choice, Quot.sound — and that a comparator confirmed the formal statement matches mathlib's own statement of FLT, which closes the standing objection that a formalisation may certify the wrong proposition. CHECKED — from the publication and the named reviewer; #print axioms was not run independently here.
| Artifact | Result | What sits outside the Lean object | Word used |
|---|---|---|---|
| Axiom Math · 3 Sep 2026 | H1 ≤ 212 | five equidistribution estimates, bilinear Bombieri–Vinogradov, the Harman decomposition, the variational certificate | hypothesis |
| OpenAI · PrimeGaps186 | H1 ≤ 186 | Deligne's Kloosterman bound, a correlation bound, 152 numerical bounds | axiom |
| Anthropic · 4 Sep 2026 | FLT | nothing beyond Lean's own three | — |
§5 argued that the standardisation window is open because the proof-exchange layer has no vocabulary, and §8 concluded that one cannot say which of two Lean artifacts assumes more. The second claim was wrong, and in an instructive way.
A machine-generated, directly comparable statement of exactly what a Lean development rests on has existed the whole time, in one command: #print axioms. Its output is the unit. It is not proposed, not standardised, not new — it is already implemented and simply not quoted. The third artifact quotes it. The first two do not.
So the diagnosis changes. This is not a missing standard. It is an existing standard with no disclosure convention, which is a different and cheaper problem: the fix is a norm requiring the axiom list to be printed alongside any claim of formalisation, not a new keyword.
The terminological argument of §§1–2 is not dissolved by this; it is confined to the place where it actually bites. #print axioms reports that a dependency is external. It cannot report what kind of external thing it is. In the second artifact's list, Deligne's bound — proved in 1974, and among the most heavily scrutinised results in the subject — prints identically to a numerical bound established only by the authors' own computation. Both appear as axiom.
That distinction is what a reader needs and what no existing term carries. The four words of §1 divide by who owes the work; what is needed is a division by where the proof lives and how well attested it is — and the fact that the two are constantly confused is why the same relation drew hypothesis from one team and axiom from another in the same week.
Revised recommendation. Not a new keyword. A required disclosure — the axiom list printed with the claim — plus a typology of statuses within that list. The disclosure is free and already exists; only the typology has to be built.
Fermat's marginal note of c. 1637 is the canonical instance of the object this note is about: a step asserted as proved, with the proof placed outside the container, and the container named as the obstacle — the margin was too narrow. It is also the canonical failure, since no such proof was ever found and the claim stood open for three and a half centuries. By the condition proposed here, an assertion of that form with no resolvable source is not an external citation at all; it is a sorry wearing a citation's clothes.
It was discharged, formally, with no external dependencies whatever — and signed off by the mathematician whose own FLT formalisation project is scaffolded on literal sorrys.
Every figure to this point was measured on one author's corpus, and §12 has flagged that as the binding weakness. This section reports the first measurement taken outside it. It is small — one mailing-list thread, six utterances, one reference manual, and one negative search — and it is described as a probe, not a corpus.
The Isabelle/Isar reference manual defines sorry as a “fake proof” that “pretend[s] to solve the pending claim without further ado”, and states what happens to the result:
“Facts emerging from fake proofs are not the real thing. Internally, the derivation object is tainted by an oracle invocation, which may be inspected via the command thm_oracles.”
thm_oracles is Isabelle's #print axioms. It reports what a theorem's derivation actually rests on, it long predates the Lean ecosystem, and it is not routinely quoted either.
§9 concluded that the shared unit already exists in Lean and simply goes unreported. The Isabelle evidence shows the same mechanism in a second mature system, thirty years older. So the finding is not that one community failed to adopt its own tool. It is that two independent systems each built the disclosure mechanism and neither community built the convention of using it. A norm that fails to form twice, independently, is a stronger result than a norm that never existed.
§4 named Isabelle as the corpus that would separate the two accounts of why the vocabulary appeared when it did. Isabelle's sorry is much older than Lean's and its collaborative-formalisation practice much smaller. If the count-noun paradigm travels with the word, Isabelle should show it. If the paradigm is generated by large collaborative projects, Isabelle should not.
From the Isabelle users list, August 2022, and the project's own release notes:
| Speaker | Form used |
|---|---|
| list participant | “theorems … that depend in some way upon “sorry”” — quoted, as a keyword string |
| M. Wenzel (Isabelle maintainer) | “The keywords “sorry” and “axiomatization”” |
| L. Noschinski | “some (invalid) sorry'd theorem” — participle, attested |
| Isabelle NEWS | “unfinished/failed future proofs” — the official noun phrase |
No plural. No numeral. No determiner plus noun. A search for sorries in Isabelle contexts returns nothing. The participle exists (sorry'd, beside mathlib's sorried); the count noun does not.
Isabelle has had the word for decades and never grew the paradigm. mathlib, with Polynomial–Freiman–Ruzsa-scale collaboration, has the full one: two sorries, these sorries, sorry-free. The word does not carry the grammar. The collaborative practice generates it. On this evidence the throughput account of §4 survives its own test and the conceptual account does not explain the split alone.
Isabelle's noun for the object is not sorry at all. It is oracle — the derivation is tainted by an oracle invocation — and unlike every term in §1 it is machine-checkable, because thm_oracles prints it. The surrounding vocabulary is likewise its own: fake proof, tainted, unfinished/failed future proofs.
This bears directly on the coining exercise recorded in book6/wp94-coining-note.md. That note proposed a new token for the relation proved elsewhere, unreadable from here. Isabelle may already hold the incumbent: a term in use for thirty years, with tooling behind it, that names precisely a derivation resting on something the checker did not verify. A proposal must now beat oracle, not merely fill a vacancy — and the honest reading of the last three findings is that each has narrowed the case for coinage and strengthened the case for disclosure.
Six utterances from one thread, one manual, one negative search. It cannot establish frequency, it cannot date the participle, and it says nothing about Coq, Agda or the avionics literature. What it does establish is that the §4 test is runnable, that it returns an answer, and that the answer is not the one flattering to the framework this note started with.