A clerk in Madras sent Hardy a hundred and twenty theorems and almost no demonstrations. Hardy’s first move is the one this corpus needs, and the man down the corridor supplies the reason it works.
The letter is dated the sixteenth. Nine pages, and across it and the one that follows some hundred and twenty theorems, written out flat, one after another, by a shipping clerk in Madras who had no university degree. Many of them were unlike anything Hardy had seen. Almost none of them came with a proof.
Hardy was, by common consent, the most exacting analyst in England. He had spent his career insisting that a result is not a result until it is demonstrated. He read the pages, decided some of the formulas “seemed scarcely possible to believe”, and on the eighth of February he wrote back.
That same year, in the same college, Alfred North Whitehead and Bertrand Russell brought out the third volume of Principia Mathematica — a book that spends some three hundred and sixty pages arriving at the proposition that one and one make two, and does so on purpose. It is the most extreme statement anyone has ever made that nothing counts until it is derived. Volume I had appeared in 1910, Volume II in 1912, Volume III in 1913.
So at one address, in one year: the highest pitch of proof-discipline ever attempted, and nine pages of unproved assertion from six thousand miles away. Hardy knew both men — he would later write a book about Russell's dismissal from Trinity — and he did not treat the two as opposites. He treated them as two different questions.
Asked later why he had believed the continued-fraction formulas before he could prove them, Hardy gave the reason that has been quoted ever since: they “must be true, because, if they were not true, no one would have had the imagination to invent them.” That is an argument from the improbability of the forgery. It is a very good argument. It is not a proof, and Hardy never said it was — he said it about his belief, and then he went and did the work.
And when the work was done he kept score, publicly. Some of Ramanujan's claims were wrong — the results on counting primes among them. Some were already known. The rest were new, and several of them opened fields. Hardy sorted the nine pages into those three piles and said which was which.
Hardy neither granted the theorems nor withheld them. He kept two ledgers — what he believed, and what had been demonstrated — and he never let an entry in the first stand in for an entry in the second. That is the whole of the discipline, and it costs one sentence per result.
This corpus cites Lean proofs by file name. tools/lean_addresses.py asks a
narrower question than it sounds: does a file of that name exist under the roots it was
given? Run live, over the geometry repository and AXLE — two roots:
Twenty-three pages send a reader to Chain.lean, and a reader who looks where this
corpus tells them to look does not find it. What that does not establish is that no
such file exists: more than twenty repositories have not been searched, and a root not passed
is a root not searched. The honest present state of every one of these 66 names is
unresolved, not absent.
The standing rule in this repository is never report absence from a single search. Two roots is a single search. So the count above is a statement about where we have looked, and the rest of this page is about what follows once a name is confirmed absent — which for these 66 is work not yet done. The sequence matters: search the roots, then apply the analysis. Not the other way round.
The roots have now been searched. All eleven in
tools/corpus_roots.txt, not two: AXLE, geometry, GTCT, vol1-proofs, 3M, dnls, b3s,
the three grossi-ops repositories and io-clone.
36 names resolve nowhere. 2 resolve only under another
case. 5 resolve upstream in Mathlib and were never this corpus's claims at all —
GrothendieckGroup.lean, ClassGroup.lean,
ClassNumber.lean, Convolution.lean, Deligne.lean, cited
correctly by WP-82 and Book IV. 74 citations in all.
The two names at the top of the table above are among those that
resolved. Chain.lean, the one cited by 23 pages, is at
GTCT/Chain.lean, with two further copies in that repository.
ZeoliteCommutation.lean is at
io-clone/zeolite_operator_order/ZeoliteCommutation.lean, the eleventh root. Its
axiom report sits in this repository at
tools/verify-audit/2026-09-09/ZeoliteCommutation.axioms.txt, and the gate beside it
reads: OK: 6 theorems, no sorryAx, no axiom outside the permitted set.
So a reader sent to Chain.lean can now be told where to
look, and a reader asking whether the zeolite theorems are proved has a kernel report to read.
Both were in the unresolved column for one reason: nobody had passed the other nine roots. That
is the whole of the R15 discipline and it is also Hardy's — the two ledgers stay separate,
and an entry moves between them when somebody does the work, not when somebody asserts it.
Say a name does come back absent after a real search. The repository has been filing such things as defects to repair, and that phrasing does quiet work. “Repair” implies there is something there to be mended. It is the same instinct that led Meinong, in Russell's day, to answer “the present King of France is bald” by saying the King must somehow subsist, or the sentence would be about nothing at all.
Russell's reply, in the paper he published eight years before the letter from Madras, was that the sentence is not about a King. “The F is G” says three things at once: there is at least one F; there is at most one F; and whatever is F is G. With no King at all, the first clause fails, and the sentence comes out plainly false. Nothing has to subsist. Nothing is meaningless.
The puzzle that had made people reach for ghosts — that “the King is bald” and “the King is not bald” both look false — dissolves, because those two sentences are not each other's negation. Block [1] evaluates all three readings over every pair of predicates on domains up to four elements:
Apply it to a citation. “The proof in X establishes P” unpacks into:
there is such a file; there is exactly one; and what it contains establishes P. If the
first clause is false, the whole sentence is false — not unverified, not pending,
not awaiting restoration. That is the payoff, and it is conditional on the search, which is
why the search has to come first. Until then the first clause is not yet evaluated,
and the corpus has a tag for that: OPEN.
Russell's second point is the practical one, and block [2] checks it. “X is not proved in AXLE” has two readings that come apart exactly when the file is missing:
| reading | says | file missing | file present, insufficient |
|---|---|---|---|
| narrow | there is a proof there, and it does not establish X | false | true |
| wide | it is not the case that there is a proof there establishing X | true | true |
So a correction written as “the proof there is incomplete” concedes that a proof exists, and is false when the file is missing. The true sentence is the wide one, and it is shorter: there is no such file. Every retraction of a dangling citation in this corpus should be written that way, and some have not been.
This very page names Chain.lean and ZeoliteCommutation.lean, and so
does ch-gelfand, which names the second one precisely in
order to say that it does not rely on it. A tool that counts names would count all
three as citations. They are not citations. Naming a thing to report that it is
missing is mentioning it, not using it.
And lean_addresses.py has handled this from the start: it exempts by
(page, name) pair, never by name alone, with the note that
“a blanket name exemption would hide a real dangling citation elsewhere.”
That is Russell's use/mention distinction, implemented, correctly, by someone who did not stop
to name it. Adding ch-gelfand's pair took ZeoliteCommutation.lean from twelve
citing pages to eleven. The name did not become less dangling — one of the twelve was
never using it.
Four sentences, and the corpus can go on saying the same true things it already believes. The first two apply only to a name confirmed absent; the third is what to write before then:
| instead of | write | because |
|---|---|---|
| “proved in X”, X confirmed absent after a full search | “there is no X; the result is asserted here and not demonstrated” | the first is false as printed |
| “proved in X”, X not yet looked for everywhere | “asserted at an address this corpus has not resolved” — and search | unresolved is not absent |
| “the proof there is incomplete” | “there is no proof at that address” | narrow scope concedes the proof |
| “pending restoration” | “believed, undemonstrated” — and put it in the other ledger | Hardy, 8 February 1913 |
None of this says the mathematics is wrong. A false citation is a fact about the citation, not about the theorem it points at — the theorem may be true, may be provable, may be proved somewhere the tool cannot see. That is exactly the position Hardy was in with nine pages in front of him and no demonstrations, and he did not resolve it by deciding. He asked for the proofs, believed what he had reason to believe, and wrote down which was which.
The corpus already keeps that ledger — “proof” in 422 chapters, “unproved” in 26, “without proof” in 11. What it has been missing is the rule for the sentence at the other end, and a nineteen-oh-five paper about a bald king supplies it.
| Russell 1905 | B. Russell, “On Denoting”, Mind 14. The theory of descriptions; developed in Principia Mathematica Vol I, Introduction ch. III (Incomplete Symbols) and ∗14. |
| Hardy–Ramanujan | Ramanujan's first letter to G. H. Hardy, 16 January 1913 — nine pages, some 120 theorems across the first two letters, almost no proofs; Hardy's reply of 8 February 1913 asking for demonstrations; his remark that the continued-fraction formulas “must be true, because, if they were not true, no one would have had the imagination to invent them”; and his sorting of the claims into wrong, already known, and new. |
| Principia Mathematica | A. N. Whitehead and B. Russell, Vols I–III, Cambridge University Press, 1910, 1912, 1913. G. H. Hardy's later account of the Trinity affair, Bertrand Russell and Trinity, is the connection between the two halves of this story. |
| in-corpus | Book 7 · Ramanujan · Whitehead & Russell · The Range of a Variable · tools/lean_addresses.py · R11 in CLAUDE.md |
| verification | book6/ch-the-present-king-of-france-verify.py — six blocks, standard library only. Every number on this page is printed by it. |
The 66 are unresolved, not absent, and this page does not claim otherwise. The run behind the table passed two roots — this repository and AXLE — while more than twenty others exist and have not been searched. Under R15 that is a single search and settles nothing about absence. Everything after the measurement is written as a conditional for that reason.
A citation being false is a statement about the citation and not
about the theorem. The counts inherit the limits of lean_addresses.py: it asks
whether a file of that name exists under the roots it was given, not whether a
declaration inside it exists or elaborates, and a root not passed is a root not searched. The
use/mention exemptions are curated by hand, so the citation count is only as good as that
curation. Strawson's 1950 objection to Russell — that such a sentence presupposes rather
than asserts existence, and so is neither true nor false — is not addressed here and is
not obviously wrong. No priority is claimed for anything: “On Denoting” is 1905 and
the letter from Madras is 1913.