The Theorem and the Reader

Terence Tao has made the point, in substance, that we can now generate theorems in enormous quantity, and that the binding constraint is no longer production but the limited number of people able to make sense of what has been produced. This paper takes that seriously by treating one corpus as a specimen and asking what its numbers actually measure. The answer is uncomfortable and, I think, general: the checks that mechanise are exactly the checks that cannot tell you whether a statement means anything; the check that can is the one that does not scale; and in a single-author corpus the count of statements examined by anyone other than their author is not merely low but structurally close to zero.

Production stopped being the constraint

For most of the history of formalisation the bottleneck was writing the proof. Getting a non-trivial argument past a kernel took months, and the number of formalised theorems was a reasonable proxy for the amount of mathematics a community had digested, because someone had digested every one of them on the way in.

That proxy has broken. With proof assistants, tactic automation and language models in the loop, declarations can be produced at a rate no reviewer matches. The number of statements in a repository now measures machine time, not human understanding. Tao’s observation is that the scarce resource has moved: not proofs, but readers.

This is not an argument against machine assistance, and this corpus is built on it. It is an argument that the metrics inherited from the era of scarcity have quietly stopped measuring what they used to measure, and that continuing to publish them is a way of overstating without ever saying anything false.

And what each one does not settle

A formal corpus admits three mechanical checks. They are genuinely useful, they are cheap, they run without a person, and they are ordered by strength. None of them is about meaning.

Check	Cost	Rules out	Does not rule out
It compiles	Seconds to minutes, automatic	Syntax and type errors	That the proof is admitted. sorry raises a warning; the build exits 0.
It is sorry-free	A text scan	An explicit hole left by the author	That the statement is empty. theorem X : True := by trivial is sorry-free.
The kernel accepts it	One #print axioms per declaration	Admitted proofs, and reliance on undeclared axioms	That the statement asserts anything at all.

Note the shape. Each check closes the loophole the previous one left open, and the sequence terminates one step short. The kernel certifies that a proof establishes its stated proposition. It has nothing whatever to say about whether the proposition is worth establishing — or whether it excludes any state of the world.

That last gap is not a technicality. It is precisely where machine-generated mathematics fails, because a generator optimising for “compiles, no sorry” is optimising for a target that a vacuous statement hits perfectly.

Statements that pass every mechanical gate and exclude nothing

DATA Four instances found in this corpus and withdrawn. Each compiled. Each was sorry-free. Each would have reported a clean axiom set.

Declaration	As stated	Why it is empty
whitneyFold_conditional	(hσ : IsMorseCritical σ ρ) : ∃ φ : ℝ → ℝ, True	φ = id discharges it for every hypothesis. The hypothesis constrains nothing.
reeb_orbit_is_integral	1 = 1	The name describes a geometric fact; the statement is an identity on numerals.
limitCycle_exists_auto	True	Proved by trivial. Carried no sorry because there was nothing to guard.
witness_codimension	5 - 4 = 1	Truncated subtraction on natural-number literals. Closes by rfl whether or not any claim about normal bundles holds.

The pattern is consistent and it is the crux of this paper: the name carried the mathematics and the statement carried none of it. A reader skimming a verification table sees reeb_orbit_is_integral · kernel-checked · ✓ and imports the meaning from the identifier. The kernel imported nothing, because there was nothing to import.

Nothing mechanical caught these. They were caught by someone opening the file and reading the proposition — the exact resource Tao identifies as scarce.

One corpus, counted honestly

DATA 28 August 2026, across thirteen repositories, eight of them reachable at the time of the sweep. Regenerated by python3 tools/theorem_census.py <repo>, which strips comments before matching, so a declaration named in a docstring counts as prose. These figures change weekly and are not the claim of this paper; the shape they make is.

Quantity	n	Share of written	Who or what produced the number
Declarations written	2,234	100%	A text scan. Measures machine time.
Sorry-free in source	1,984	88.8%	A text scan. Measures whether a hole was left explicitly.
Individually kernel-audited	173	7.7%	A probe that ran. Measures what a machine confirmed.
Admitted and disclosed	250	11.2%	Honest open obligations.
Axiom declarations	52	—	An axiom is not a proof.
Read and judged by the author	2,234	100%	He wrote them. This number is uninformative by construction.
Read and judged by an independent reader	not tracked, and near zero	≈ 0%	Nothing. No repository records it, and for a single-author corpus there is little to record.

The last two rows are the point, and the distinction between them is the whole argument. Counting declarations the author has read gives 2,234 — a perfect score, and worthless, because an author reading his own statement is checking his intent against his notation, not checking whether the statement means what a stranger would take it to mean. The four withdrawn declarations of § 3 survived years of exactly that kind of reading. They did not survive the first reading that approached the proposition without already knowing what it was supposed to say.

So the informative quantity is the second one: declarations read and judged by someone other than the author. For this corpus it is not tracked, and it is close to zero — not through neglect but structurally. One author, one machine-assisted pipeline, no editorial board. The tooling in this paper can raise the kernel tier arbitrarily; it cannot manufacture a second reader.

It is worth being exact about what does not count as one. The author’s own second pass is the same reader on a later day. A language model in the loop is not an independent reader either: it is part of the production pipeline, it is what made the statements plentiful, and treating its agreement as review is circular in the same way that grading one’s own paper twice is. Machine assistance is what created the surplus; it cannot also be what certifies the surplus.

The distribution across repositories sharpens it. The repository with 1,407 declarations has nineteen audited and no continuous integration on any branch. The repository with nineteen declarations has sixteen audited and CI on every push. Verification coverage runs inversely to size, which is what one expects when checking is human-paced and writing is not.

Why the ratio inverts

Set the costs side by side, in orders of magnitude rather than precise figures.

Operation	Cost per declaration	Scales with
Write a declaration, machine-assisted	Seconds to minutes	Compute
Compile it	Milliseconds, amortised	Compute
Kernel-audit it	Milliseconds, amortised	Compute
Scan it for a trivially inhabited conclusion	Milliseconds	Compute
Read the statement and decide whether it says anything	One to ten human minutes	People

Four rows scale with hardware; one does not. So a corpus grows until the reading backlog dominates, and then keeps growing, because nothing in the pipeline exerts back-pressure. The mechanical checks all stay green throughout — they are measuring the cheap rows.

MODEL On these figures, auditing everything written in this specimen is roughly a fortnight of compute. Reading everything written is, at five minutes each, something like six person-months. That gap is the phenomenon, and no amount of additional automation narrows it, because automation adds to the numerator.

Duplication accumulates faster than pruning

DATA Grouping version-suffixed copies reduces the largest repository’s 1,407 declarations to 765 — forty-six per cent of the raw count is the same material at different vintages. One file exists in four places, two byte-identical and two divergent; one script exists in seven.

Deciding which copy is canonical is not a mechanical operation either. It requires knowing what the project meant to keep, so it queues behind the same scarce resource. Meanwhile the duplicates inflate every scan-based figure, which is one reason a corpus of this kind reports larger numbers the less carefully it is read.

A related instance, small but exact: one file in the corpus is Lean source carrying a version number where its extension should be. No build system compiles it, no counter counts it, and a citation naming it resolves to nothing — while the file itself is perfectly good source. It went unnoticed because noticing required someone to look, and everything mechanical was looking for *.lean.

Report the readership, not only the yield

Four consequences, stated as practice rather than principle.

Publish the three counts separately, and never let the largest wear the strongest word. “Written”, “sorry-free” and “kernel-audited” differ here by more than an order of magnitude. A page presenting a written-tier number under the heading proved overstates by two full steps without containing a single false sentence.

Attach a producing command to every published figure. A number no script regenerates is a number a reader must take on trust, and in a corpus that changes daily it will be wrong within the week whether or not anyone notices.

Treat the identifier as untrusted. The four withdrawn statements in § 3 were all discovered by reading the proposition after having read the name. Verification tables invite the opposite habit. VALUE PREMISE A name is a claim about a statement and should be audited like one.

Name the reader, and require that it not be the author. OPEN The proposal this paper actually makes: alongside the kernel tier, record which declarations have been read and judged non-vacuous by a named person who did not write them, with the date. A self-reported reading is not a datum; the author’s pass is already implicit in authorship, and a model in the loop is part of production, not review. It is a weaker guarantee than a kernel check, far more expensive, and unfakeable in exactly the way the mechanical tiers are not — nobody can regenerate it overnight. It is the only tier that responds to Tao’s objection, and this corpus’s honest current value for it is essentially zero.

VALUE PREMISE Peer review is the institution that has always supplied independent readers, and its scarcity is the same scarcity described here. Machine assistance multiplied one side of that exchange and not the other. A corpus that grows past what review can absorb has not become better verified; it has become harder to referee, and should say so in its own figures rather than leave a reader to infer it.

Four disclaimers

It does not claim machine assistance is the problem. Every check in § 2, and every figure in § 4, exists because machines produced it. The argument is about which metrics survive the change in what is scarce.

It does not claim the specimen is representative. It is one corpus, single-author, uneven. It is offered because its numbers are open and its failures are documented, not because it is typical.

It does not claim a fix. “Name the reader” is a bookkeeping proposal, not a solution to the comprehension bottleneck. Nothing here makes mathematics easier to understand.

It does not claim these numbers. They are dated 28 August 2026 and change weekly. The commands in § 9 are the durable part.

Every figure, regenerated

Figure	Command
Written / sorry-free / admitted / axiom declarations	python3 tools/theorem_census.py <repo>
Per-file basis and version-duplicate groups (§ 6)	python3 tools/theorem_census.py --table <repo>
Kernel-audited counts	bash tools/verify-*/run.sh
Vacuity scan and its fixtures (§ 3)	cd vol1-proofs && bash tools/run.sh
Agreement of probe, runner and README counts	python3 tools/probe_consistency.py
Whether a cited declaration resolves at the path cited	python3 tools/decl_resolve.py claims.json <repo>
The registry page	python3 scripts/build_theorem_registry.py

Two of these found defects on their first run — a count guard found a README stating twelve where the runner had been pinned at twenty-eight, and the census found the extensionless module of § 6. Neither defect was subtle. Both had survived because no one had looked, which is the paper’s thesis in miniature.

Where this sits

WP-78 · The Seam and the Boundary — artifacts that live only inside the documents citing them; the audit tools cannot see past the boundary of the repository.

WP-79 · The Ratio and the Scale — which dm³ quantities an experiment could refute. WP-79 asks what the world can say about our claims; this paper asks what we can say about them ourselves.

Project 1080 — the AXLE Theorem Registry, the three-tier publication of these counts. AXLE — Algebraic eXpression Language for Evaluation, the Lean 4 / Mathlib4 environment. github.com/TOTOGT/AXLE