Finding 1
Citations concentrate on papers the Lean library skips
Cross‑references were extracted from the LaTeX sources of all 746 manuscripts that ship a build/ tree, using two independent signals: the full preprints/<dir>/<file>.pdf URL and the OAI:<dir> citation key. Cross-references pointing at a superseded revision are redirected to the revision that replaced it. That gives 719 manuscripts joined by 591 citations. The graph is mostly empty and a few papers carry it: 223 manuscripts cite nothing in the collection and are cited by nothing, while one paper is cited 16 times and two more are cited 7 and 6.
Most-cited manuscripts — times cited by other manuscripts in the collectionbar length = in‑degree, to scale
has a Lean entry
no Lean entry
Finding 2
The catalogue grades its own work "unchecked"
lean/formalization.yaml is the machine-readable catalogue of what has been formalized. Its own metadata reads review: status: unchecked and status.scope: "Partial progress.", with automation.methods: [agent]. A Lean entry means a compiler accepted a declaration pointed at by a comparator config. It does not mean anyone checked that the declaration states the theorem the paper claims. "Formalized" and "verified" are two different claims, and only the weaker one is being made.
Finding 3
Three different denominators for one coverage number
The README and history.md both say 300/719 top-line results formalized, about 42%. The catalogue enumerates 173 sources plus 30 related_formalizations. And the family map resolves to 135 of 372 families containing at least one formalized member. All three are defensible readings of the same corpus, and none of them is stated anywhere alongside the others. Until they reconcile, "42%" is not a quantity you can reason with.
Finding 4
The three withdrawals were scrubbed clean
A sign error in a stabilization‑trace argument took down three manuscripts on 6 October. Searching every .tex, .bib and .md file in the tree finds zero references to them from any surviving manuscript, and they are absent from CONTENTS.md and overview.tex. The removal is tidy; the trail is not. A reader browsing the manuscript map cannot tell the Hodge/K3 line lost three results, because only the flat changelog in history.md records it.
The withdrawn proofs remain recoverable, though. Their sources are gone from the working tree but present at the archived revision the notices cite, which is reachable in the repository's object store — git ls-tree -r adc7f124 -- preprints/Algebraicity-of-Weil-classes-on-split-abelian-eightfolds-September-18-2026 lists the full section files. The withdrawal reasoning itself is therefore checkable against the text, and nobody appears to have done it.
Finding 5
Version history is on disk but unlabelled