THE VERSION DELTA TABLE
what moved in Mathlib between two releases
Every other measurement here is a snapshot. This is the first that needed two, and it answers a question that could not be asked before: what happens to a formal library's trusted base when it ships a release.
For v4.32.1 to v4.33.0 the answer is that the trusted base did not move. The axiom roster is the same 15 axioms on both sides. Everything else grew.
Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 against Lean 4.33.0 with Mathlib v4.33.0 (tag db584cd6) · the same extractor on both sides
| quantity | v4.32.1 | v4.33.0 | delta | note |
|---|---|---|---|---|
| declarations | 790,171 | 795,218 | +5,047 | — |
| theorems | 532,605 | 535,601 | +2,996 | — |
| definitions | 228,875 | 230,757 | +1,882 | — |
| others | 28,676 | 28,845 | +169 | — |
| axioms | 15 | 15 | +0 | — |
| modules | 10,511 | 10,599 | +88 | — |
| declarations added | — | 12,432 | +12,432 | present in the new version only |
| declarations removed | 7,385 | — | -7,385 | present in the old version only |
| statements changed | — | — | +15,994 | same name, different statement dependencies — a different claim |
| reproved only | — | — | +24,172 | same statement, different proof dependencies — same claim, new proof |
| moved module | — | — | +835 | same name, relocated |
| axiom roster | 15 | 15 | +0 | unchanged: Classical.choice, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, Quot.lcInv, Quot.sound, isScalarObj, lcAny, lcCast, lcErased, lcProof, lcUnreachable, lcVoid, propext, sorryAx |
statements changed and reproved only are both computed over declarations present in both releases under the same name. A changed statement means the declaration's type dependencies moved, so it is a different claim wearing an old name. reproved only means the statement held and the proof dependencies moved.
Get the data
version-delta.json · version-delta.csv · CC-BY-4.0 · version 2026-08-12
One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move. Cite the series as 10.5281/zenodo.21900625, which resolves to the current deposit.
Reproduce it
lake env lean -D maxErrors=4000 Split.lean # once per release python diff_dumps.py OLD.tsv NEW.tsv --old-label v4.32.1 --new-label v4.33.0
A Mathlib dump takes roughly twenty minutes and 650 MB per side. Method: 10.5281/zenodo.21769846.
The trusted base held
The axiom roster is identical across the release: 15 axioms, none added, none removed. That is the sentence anyone depending on Mathlib wants and nobody could state before, because stating it requires measuring both sides with the same instrument rather than reading a changelog.
It is also the row most worth re-running every release. An axiom appearing is the one change to a library that no test suite catches and no diff summarises.
Proofs churn faster than the library grows
24,172 theorems kept their exact statement and got different proof dependencies. Net new theorems over the same release: 2,996. Proof churn runs roughly 8x growth.
Neither number is visible to a text diff. A diff sees a file changed; it cannot see that a theorem's proof dependencies moved while its statement stood still. That distinction is the whole reason to compute this from a provenance dump.
It also bounds how stale a provenance measurement gets. Any figure about what proofs rest on is measuring a population that turns over at this rate, which is the argument for republishing per release rather than citing a number from a year ago.
What this does not say
It does not say the reproved theorems changed what they rest on. A different proof can reach exactly the same axioms. Establishing that requires computing the closure on both sides, which is a separate and much more expensive measurement than this one.
Two dumps from different extractors cannot be compared, so both labels are recorded in the data. The comparison here used one extractor across both releases.