Macroscopic quality signatures of Lean formalization projects

Every corpus row is measured on the exact tier: a Lean metaprogram walks the elaborated environment and reads getUsedConstants off every declaration's type and value — capturing instance uses, notation-mediated references, and dot-notation that textual analysis cannot see. Proof dumps that ship no lakefile were given one (or measured on the subproject that ships one); corpora whose files name-collide are loaded one module per environment and merged. A repo that cannot be built at all is excluded rather than approximated — the earlier textual (parser-based) tier survives only as a cross-check, quantified in §13.

If reuse is Mathlib's central design philosophy, the right measurement is not how often a declaration is cited but how much work sharing avoids. Define the fully-inlined cost of a declaration recursively — cost(v) = 1 + Σ cost(deps), with repetition — the size its dependency tree would have if every lemma were re-proved at every use site. In a flat corpus this is chain length; in a shared library it grows exponentially, so we report log₁₀ cost: the number of orders of magnitude of duplication that sharing eliminates.

This is the metric most entangled with size — it correlates with log-declarations at ρ = +0.79 and fails the discriminant test of §14 (the three largest uncurated corpora out-compound the reviewed median purely from bulk), so it is badged a size proxy, kept out of the composite, and shown raw as a descriptive measure.

The base metric: for each reusable declaration, how many distinct other declarations in the same repo reference it. The tail tells the real story — every corpus has hubs, but only libraries have a thick middle: thousands of declarations each reused a handful of times across many files.

The heartbeats hypothesis — that low-quality corpora make the elaborator work harder per line — measured by re-elaborating sampled built files with import-loading baselines subtracted. The result inverts the hypothesis: shallow or sorried content elaborates cheaply, while high cost tracks genuinely hard mathematics being worked. Cost is an effort meter, not a quality meter; the smell is expensive-per-line combined with nothing-reused.

Rather than fitting to labels, this section lets the metrics speak jointly: a PCA of the battery (no imputation — only metrics computed for every corpus repo enter), and an unweighted composite of the mechanical checks. Both are built from raw values of the discriminant-valid metrics only (§14): checks on which a huge uncurated corpus scores high from bulk alone (the amortization exponent, depth, mean in-degree) are excluded, so a repo cannot score well just by being large. Neither is a quality certificate; §12 documents the Gauss-PR case where every mechanical check passes and community review still said no.

A reference in a statement (a type) or a definition body is load-bearing: it shapes the API others must build on. A reference inside a proof is erasable. Layered mathematics shows up as theorems cited by other statements and definitions built on definitions — proof-dump corpora cite lemmas only inside proofs.

For repos downstream of Mathlib, leaning on it is a virtue: more upstream references per declaration and a broader vocabulary of distinct Mathlib lemmas mean less reinvention. The scatter shows Mathlib references per declaration against the share of declarations never reused internally — the lower-right corner (heavy leverage, everything reused) is where good libraries live.

How broadly is reuse spread? The share of declarations reused at least twice captures the thick middle of the CCDF in one number, and the top-1% share captures the opposite failure mode: a few hub declarations absorbing all reuse while the rest is dead weight. (The longest build-on chain now lives beside the amortization exponent in §2 — depth is the chain view of the same compounding phenomenon.)

Duplication is anti-reuse: the same normalized declaration body appearing more than once. And a sorry is an unproved claim — fine in a statements-only conjecture list, disqualifying in a corpus presented as proven mathematics.

Software engineering has measured code quality for fifty years; the honest summary of that literature is that volume-derived indices predict quality poorly — McCabe's cyclomatic complexity rests on weak theoretical footing, and the composite Maintainability Index is widely criticized for averaging away the power-law tails where risk lives — while process signals (churn, review activity) and threshold "risk profiles" (the SIG maintainability model) hold up empirically. The adaptations below follow that lesson: keep the simple, distribution-aware checks; skip the composite indices.

Ilin & Nugent's expert-review case study (arXiv:2606.13925) examined a semi-autonomous formalization of Grothendieck's vanishing theorem — a project that is in this corpus (half of Clawristotle) — and found that compiling, sorry-free code still failed expert review on four axes. That gives us a rare labeled instance to test against:

In an earlier revision we also measured Math Inc's Gauss PR against the community Sphere Packing repo (same theorem, different process). It passed — indeed topped — every mechanical check in this study: sorry-free, 94% docstring coverage, low duplication, well-organized cross-directory reuse. Community review nonetheless rejected it, citing exactly the definition-quality and API-design axes above; the only residual quantitative tells were the narrowest Mathlib vocabulary per citation in the corpus and a heavier proof-length tail than its target repo. It is excluded from the corpus here at the community's judgment, and it is the strongest caution this study can offer: a modern AI pipeline can saturate every mechanically checkable signal while failing expert review.

The scorecard is humbling and confirms the paper's thesis: Clawristotle lands near the top of our composite (2nd of 25) — structural metrics see its clean file-level organization and zero duplication, and are blind to the definition-quality and API-design deficiencies the reviewers found. Two of four issue classes are partially visible (organization; reusability via never-reused definitions), two are invisible (definition quality, theorem generality). Mechanically checkable metrics bound quality from below; they do not certify it. The GitClear findings on AI-assisted code — clone blocks up 4–8×, cross-file calls down 35% — are the software-engineering shadow of the same phenomenon, and match the two metrics this study found most discriminating.

Earlier iterations of this study approximated unbuildable repos with a textual tier (a scoping parser over source text). Every corpus row is now measured exactly, but the comparison remains useful as a validity check on the instrument: for every repo measured on both tiers, we compare them metric by metric — the cross-tier Spearman correlation of repo values and the median absolute difference. Rankings agree strongly on hygiene and locality metrics; absolute levels differ most where the exact tier sees what text cannot (instance and dot-notation references inflate exact in-degrees), and the amortization exponent is not recoverable from text at all — the finding that forced the exact-only corpus.