Book XIX · Chapter 4 · 2026-09-27 · Provenance
MATHEMATICS · FORMAL VERIFICATION
Addresses
98 file names missing here, 49 missing everywhere, and a tool reading a tool
Before asking whether a proof is right, a reader can ask something cheaper: does the file the page names exist? Across this corpus, 98 file names do not resolve anywhere in the repository. This chapter was planned around a count of 110. That number turned out to be the count of files that do exist.
1 · The check
98 names, 217 citations
tools/lean_addresses.py reads the 874 published pages and matches every X.lean named in prose against the 110 tracked Lean files (109 distinct names, because two files share one) and Mathlib's 4,543. COMPUTED
- 98 names resolve nowhere, cited 217 times;
- 1 resolves only under another case: main.lean on the page, Main.lean on disk. It opens on a Mac and 404s on GitHub;
- 12 are Mathlib files cited correctly, which are not the corpus's claims.
| most-cited name that resolves nowhere | pages |
|---|
| AutophagyDm3.lean | 15 |
| PrincipiaVol1.lean | 13 |
| Chain_updated.lean | 12 |
| ZeoliteCommutation.lean | 11 |
| AutophagyDm3_v2.lean | 9 |
60 of the 98 appear on a single page. Four survive only in retired folders. Chain_updated.lean is named in this book's own Chapter 1 and index. COMPUTED
Corrected on the Mac, the same eveningThe first version of this page said 242 citations. The Mac run exposed two things. The count had included 25 citations on retired copies in _to_delete/, a folder that is neither tracked nor published, so the tool now skips it. And a census taken live keeps changing as new books add pages and Lean files. The check now runs on the repository exactly as it stood at commit e6c5e85, so any reader gets these numbers. COMPUTED
2 · The artefact
A tool read another tool
The first run today reported 99 names and 385 citations. The top entry was FILE.lean, on 96 pages. No page claims that file. The phrase comes from the one-click download box that tools/run_yourself.py (R26) writes: "then lake env lean FILE.lean". The address checker read the box as prose. COMPUTED
The fix is one line. lean_addresses.py now strips the generated blocks (po-run, po-gss, po-related, po-subject) before it scans, the same rule run_yourself.py already follows. This is the second time in a week that a generator's output leaked into another checker's input.
The planned 110
The index said "110 .lean names cited across the corpus resolve nowhere". No run of that figure was recorded. The repository has exactly 110 tracked .lean files, and the tool's header line prints "110 corpus .lean files". The plan most likely took the wrong line. It is corrected here. COMPUTED
3 · The smallest rule
Name only what resolves
The books written this session (XI, XII, XVIII, XX, XXI) cite no name that resolves nowhere. They were written after R26, whose download box links only to files that exist. If a page offers a download link, the address has to be real. COMPUTED
Proposed rule (R27)
A new or edited page may name X.lean only if lean_addresses.py resolves it. The 98 existing names are frozen as a baseline, which may shrink but never grow. PROPOSAL
With the sister repositories (run on the Mac, 2026-09-27)
lean_addresses.py . --roots ~/Desktop/AXLE ~/Desktop/GTCT scanned 906 pages against 212 Lean files in 3 roots. It found 49 names that resolve nowhere (96 citations once retired copies are excluded; the first run said 104), 2 that resolve only under another case, and 6 upstream. So about half of the 98 do exist; they live in AXLE or GTCT, not here. Those pages send the reader to the wrong repository, which is a smaller failure than naming a file that does not exist at all. The other 49 resolve nowhere at all. COMPUTED
A name that resolves is still not a correct citation. decl_resolve.py is the rung above.