THE METAMATH AXIOM TABLE

five foundations, one engine, one pinned revision

Five databases, 71,213 theorems, one closure engine. The comparison is only possible because the same program reads all five; a measure computed by five different tools would be five measures.

Assertions are separated from syntax constructors by typecode, not by name. A $a beginning |- asserts something; one beginning class, wff, term or type says a piece of notation is well formed and carries no mathematical content. Counting them together makes every total meaningless.

Measured with gonzalgo's closure engine · github.com/metamath/set.mm @ 7ddd528c948a, fetched 2026-08-13 · 71,213 theorems across five databases

database	label	role	typecode	theorems depending	share of db	entry points
set.mm	ax-mp	assertion	\|-	47,613	99.88%	5,317
set.mm	wi	syntax constructor	wff	47,611	99.87%	11,509
set.mm	ax-1	assertion	\|-	47,500	99.64%	164
set.mm	ax-2	assertion	\|-	47,479	99.6%	13
set.mm	wn	syntax constructor	wff	47,327	99.28%	8,298
set.mm	ax-3	assertion	\|-	47,272	99.16%	2
set.mm	wb	syntax constructor	wff	47,090	98.78%	13,206
set.mm	df-bi	assertion	\|-	47,087	98.77%	6
set.mm	wa	syntax constructor	wff	45,916	96.32%	27,053
set.mm	df-an	assertion	\|-	45,887	96.26%	28
set.mm	wal	syntax constructor	wff	44,872	94.13%	2,818
set.mm	ax-gen	assertion	\|-	44,589	93.53%	148
set.mm	ax-4	assertion	\|-	44,553	93.46%	1
set.mm	cv	syntax constructor	class	44,462	93.27%	23,468
set.mm	wex	syntax constructor	wff	44,413	93.16%	3,684
set.mm	df-ex	assertion	\|-	44,367	93.07%	60
set.mm	wceq	syntax constructor	wff	44,314	92.96%	28,563
set.mm	ax-5	assertion	\|-	44,119	92.55%	81
set.mm	ax-6	assertion	\|-	43,911	92.11%	1
set.mm	ax-7	assertion	\|-	43,839	91.96%	1
set.mm	wcel	syntax constructor	wff	43,217	90.65%	35,918
set.mm	ax-9	assertion	\|-	42,450	89.05%	1
set.mm	ax-ext	assertion	\|-	42,377	88.89%	7
set.mm	df-cleq	assertion	\|-	42,363	88.86%	2
set.mm	wsb	syntax constructor	wff	42,256	88.64%	513
set.mm	df-sb	assertion	\|-	42,243	88.61%	2
set.mm	ax-8	assertion	\|-	42,172	88.46%	1
set.mm	df-clel	assertion	\|-	42,097	88.31%	2
set.mm	wtru	syntax constructor	wff	42,052	88.21%	642
set.mm	df-tru	assertion	\|-	42,022	88.15%	1
set.mm	cab	syntax constructor	class	41,899	87.89%	1,922
set.mm	df-clab	assertion	\|-	41,891	87.87%	69
set.mm	wo	syntax constructor	wff	41,266	86.56%	3,618
set.mm	df-or	assertion	\|-	41,257	86.54%	76
set.mm	cvv	syntax constructor	class	41,031	86.07%	9,609
set.mm	df-v	assertion	\|-	40,756	85.49%	3
set.mm	wss	syntax constructor	wff	40,166	84.25%	11,312
set.mm	df-ss	assertion	\|-	40,099	84.11%	108
set.mm	w3a	syntax constructor	wff	39,727	83.33%	10,467
set.mm	df-3an	assertion	\|-	39,703	83.28%	508
set.mm	csn	syntax constructor	class	39,334	82.51%	6,798
set.mm	cdif	syntax constructor	class	39,296	82.43%	3,696
set.mm	df-dif	assertion	\|-	39,276	82.39%	4
set.mm	wfal	syntax constructor	wff	39,251	82.34%	171
set.mm	cun	syntax constructor	class	39,223	82.28%	2,929
set.mm	df-un	assertion	\|-	39,217	82.26%	6
set.mm	df-fal	assertion	\|-	39,214	82.26%	8
set.mm	c0	syntax constructor	class	39,203	82.23%	6,448
set.mm	crab	syntax constructor	class	39,201	82.23%	3,709
set.mm	df-rab	assertion	\|-	39,200	82.23%	193
set.mm	df-sn	assertion	\|-	39,190	82.21%	55
set.mm	df-nul	assertion	\|-	39,075	81.97%	1
set.mm	cpr	syntax constructor	class	38,916	81.63%	2,365
set.mm	df-pr	assertion	\|-	38,878	81.55%	128
set.mm	cop	syntax constructor	class	38,738	81.26%	4,180
set.mm	wral	syntax constructor	wff	38,593	80.96%	9,676
set.mm	df-ral	assertion	\|-	38,510	80.78%	257
set.mm	cif	syntax constructor	class	38,472	80.7%	2,314
set.mm	df-if	assertion	\|-	38,466	80.69%	5
set.mm	df-op	assertion	\|-	38,375	80.5%	2
set.mm	wbr	syntax constructor	wff	38,340	80.42%	15,127
set.mm	df-br	assertion	\|-	38,094	79.91%	486
set.mm	cin	syntax constructor	class	37,891	79.48%	4,422
set.mm	df-in	assertion	\|-	37,864	79.43%	11
set.mm	wrex	syntax constructor	wff	37,850	79.4%	7,513
set.mm	df-rex	assertion	\|-	37,773	79.24%	428
set.mm	copab	syntax constructor	class	37,308	78.26%	797
set.mm	df-opab	assertion	\|-	37,307	78.26%	44
set.mm	ax-sep	assertion	\|-	37,213	78.06%	15
set.mm	ax-12	assertion	\|-	36,964	77.54%	4
set.mm	ax-pr	assertion	\|-	36,879	77.36%	5
set.mm	cuni	syntax constructor	class	36,669	76.92%	2,767
set.mm	df-uni	assertion	\|-	36,627	76.83%	6
set.mm	wnf	syntax constructor	wff	36,608	76.79%	267
set.mm	df-nf	assertion	\|-	36,606	76.79%	19
set.mm	cxp	syntax constructor	class	36,400	76.36%	4,373
set.mm	ax-10	assertion	\|-	36,213	75.96%	1
set.mm	df-xp	assertion	\|-	36,164	75.86%	60
set.mm	ax-11	assertion	\|-	35,964	75.44%	22
set.mm	cdm	syntax constructor	class	35,879	75.26%	4,837
set.mm	ccnv	syntax constructor	class	35,814	75.13%	2,829
set.mm	df-dm	assertion	\|-	35,709	74.91%	15
set.mm	df-cnv	assertion	\|-	35,703	74.89%	14
set.mm	wne	syntax constructor	wff	35,594	74.66%	8,502
set.mm	wrel	syntax constructor	wff	35,500	74.47%	1,071
set.mm	df-rel	assertion	\|-	35,488	74.44%	83
set.mm	df-ne	assertion	\|-	35,449	74.36%	379
set.mm	cfv	syntax constructor	class	35,326	74.1%	24,816
set.mm	cio	syntax constructor	class	35,291	74.03%	258
set.mm	df-iota	assertion	\|-	35,279	74.0%	11
set.mm	wmo	syntax constructor	wff	35,139	73.71%	440
set.mm	df-mo	assertion	\|-	35,113	73.66%	1
set.mm	df-fv	assertion	\|-	35,071	73.57%	26
set.mm	ccom	syntax constructor	class	34,812	73.02%	2,155
set.mm	df-co	assertion	\|-	34,738	72.87%	20
set.mm	df-nfc	assertion	\|-	34,720	72.83%	15
set.mm	wnfc	syntax constructor	wff	34,720	72.83%	145
set.mm	weu	syntax constructor	wff	34,697	72.78%	495
set.mm	df-eu	assertion	\|-	34,691	72.77%	63
set.mm	cid	syntax constructor	class	34,627	72.64%	1,307
set.mm	wfun	syntax constructor	wff	34,393	72.15%	1,814
set.mm	df-id	assertion	\|-	34,308	71.97%	19
set.mm	df-fun	assertion	\|-	34,222	71.79%	9
set.mm	ax-nul	assertion	\|-	34,083	71.49%	13
set.mm	crn	syntax constructor	class	34,065	71.46%	3,887
set.mm	df-rn	assertion	\|-	33,858	71.02%	83
set.mm	cres	syntax constructor	class	33,103	69.44%	3,491
set.mm	df-res	assertion	\|-	33,064	69.36%	59
set.mm	cmpt	syntax constructor	class	32,721	68.64%	5,170
set.mm	df-mpt	assertion	\|-	32,684	68.56%	81
set.mm	cpw	syntax constructor	class	32,642	68.47%	2,648
set.mm	wsbc	syntax constructor	wff	32,638	68.46%	716
set.mm	df-sbc	assertion	\|-	32,617	68.42%	41
set.mm	df-pw	assertion	\|-	32,543	68.26%	17
set.mm	wfn	syntax constructor	wff	32,501	68.18%	3,259
set.mm	df-fn	assertion	\|-	32,284	67.72%	90
set.mm	cima	syntax constructor	class	32,058	67.25%	2,658
set.mm	df-ima	assertion	\|-	32,002	67.13%	196
set.mm	wf	syntax constructor	wff	31,785	66.67%	6,055
set.mm	df-f	assertion	\|-	31,715	66.53%	138

Showing the first 120 of 4,424 rows. Ordered by database, then by dependents. The full set is in the JSON and the CSV.

dependents counts theorems in that database whose proof closure reaches the statement, including everything inherited. entry points counts theorems whose own proof cites it directly. share of db is dependents over that database's own theorem count, so rows from different databases are comparable.

Get the data

metamath-axioms.json · metamath-axioms.csv · CC-BY-4.0 · version 2026-08-13

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

pip install gonzalgo
gonzalgo mm set.mm iset.mm nf.mm ql.mm hol.mm

Databases from github.com/metamath/set.mm at 7ddd528c948a. Method: 10.5281/zenodo.21769846.

Not one incomplete proof, anywhere

Across all five databases and 71,213 theorems, the number whose proof contains a ? step is zero. Metamath marks an incomplete proof explicitly, so this is a check rather than an assumption, and it is the claim most worth making about a formal library.

Why the typecode and not the name

set.mm names its axioms ax- and its definitions df-, and that rule agrees with the typecode on all 3,008 of its $a statements — checked, not assumed. It is still a house style. ql.mm and hol.mm use term and type typecodes with different naming, and a set.mm-trained prefix rule misclassifies them outright.

This is the general point about measuring several libraries with one instrument: the convention you learned from the biggest one is not a property of the format.

Why the revision is on the page

These databases move. Measured today, iset.mm has 38 more theorems and set.mm four more $a statements than when the earlier tables here were built, and those tables recorded no revision — so their figures cannot be reproduced exactly, only approximately.

Rule R1 of the Kernel Trust Profile exists for this: every number must be derivable by a third party from a named revision. This table names one.

The foundations, side by side

set.mm 47,672 theorems, 1563 assertions, 3008 $a · iset.mm 16,274 theorems, 493 assertions, 905 $a · nf.mm 5,976 theorems, 201 assertions, 363 $a · ql.mm 1,140 theorems, 48 assertions, 77 $a · hol.mm 151 theorems, 47 assertions, 71 $a

The largest single dependency in each: ax-mp at 99.88% of set.mm, ax-mp at 99.74% of iset.mm, ax-mp at 99.77% of nf.mm, ax-r2 at 99.56% of ql.mm, ax-cb1 at 81.46% of hol.mm