THE ENTRY-POINT TABLE
how often a library reaches for its own axioms
An axiom is cited directly by a few theorems and inherited by many. The count of direct citations is the entry points, and dividing by the library's size gives a figure that means the same thing in a database of 47,000 theorems and one of 151.
The three large databases land close together — 0.3758 (set.mm), 0.3782 (iset.mm), 0.4259 (nf.mm) — across ZFC, intuitionistic logic and New Foundations. Three communities with different foundations and no shared plan reach for their axioms at nearly the same rate. The two small databases sit far above, which is what a library looks like before its results are mostly built on earlier results.
Measured with gonzalgo · Metamath set.mm, iset.mm, nf.mm, ql.mm, hol.mm · each database's own axiom declarations and proof structure
| database | foundation | theorems | axioms used | entry points | entries / theorem | amplification |
|---|---|---|---|---|---|---|
| set.mm | ZFC set theory, classical first-order logic | 47,621 | 1,447 | 17,898 | 0.3758 | 292.1 |
| iset.mm | Intuitionistic set theory | 16,236 | 480 | 6,140 | 0.3782 | 220.5 |
| nf.mm | Quine's New Foundations | 5,976 | 195 | 2,545 | 0.4259 | 93.5 |
| hol.mm | Higher-order logic | 151 | 43 | 175 | 1.1589 | 16.7 |
| ql.mm | Quantum logic | 1,140 | 43 | 2,759 | 2.4202 | 6.3 |
entry points counts theorems citing an axiom directly, as opposed to inheriting it through another theorem. entries / theorem is that over the theorem count and is the column to compare across rows. amplification is dependents over entry points, reproduced from the published table; the next section is why it is not a column to rank on.
Get the data
entry-points.json · entry-points.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.
Reproduce it
pip install gonzalgo gonzalgo mm set.mm iset.mm nf.mm ql.mm hol.mm
The same command produces the Metamath rows of the Kernel Index; these are its remaining columns.
What amplification cannot mean
Amplification is dependents divided by entry points, and it looks like a measure of how much a foundation yields. It is not. Consider two refactorings that preserve every theorem's statement and every theorem's transitive axiom closure. Inline every citation of a lemma and each dependent now cites the axiom directly, so entry points equal dependents and amplification falls to 1. Introduce a single gateway lemma stating the axiom and reroute every citation through it, and entry points fall to one, sending amplification to the full dependent count.
So amplification ranges over the whole interval between those two extremes without a single theorem changing. The figures 292×, 221×, 94× here, and 2,256× for Classical.choice in Mathlib, describe how four communities chose to organise proofs. That they land in a similar range is a real observation about engineering practice and not one about ZFC.
This is why the column is present and the table is not sorted on it.
The extreme case
In set.mm, ax-4 is cited directly in one proof and inherited by 44,501 theorems — a single proof step carrying an axiom into 93% of the library. Most axioms there are cited directly in three proofs or fewer. Concentration like that is what makes provenance worth computing at all: the theorems that depend on an axiom and the theorems that use it are almost disjoint sets.
Why no Lean rows
Lean's axioms are fixed by the system rather than declared per library, so the nine Lean libraries in the Kernel Index share one axiom set and the comparison would be against a constant. The single Mathlib figure quoted above is stated in the paper, not derived here.