metamath_setmm — Metamath set.mm theorem dependencies (2015-2026)

Description

Dependencies between the theorems of set.mm, the main database of the Metamath project, a formalization of mathematics from first principles (classical first-order logic and ZFC set theory), with every step of every proof verified by machine. set.mm was started by Norman Megill in 1992, and has been developed collaboratively since then (on GitHub since 2015), with tens of thousands of theorems, from logic to real and complex analysis, algebra, topology and number theory.

The nodes are the assertions of the database: the theorems (statements with a proof, $p`), the axioms and the definitions (`$a statements of the form |- ...), and the syntax constructors ($a` statements of the other types, which define how formulas, classes and set variables are built, e.g. `wi` for the implication). A directed edge goes from a theorem to each assertion referenced in its proof (theorems, axioms, definitions, and syntax constructors used to build the formulas of the proof), with the number of times it is referenced. The hypotheses of the theorems (`$e and $f` statements) are not nodes, and are left out. The proofs are mostly stored in the compressed format of Metamath, where the steps reused within a proof are referenced once, so that the counts are of the references in the proof as stored (the number of times the statement is referenced in the compressed proof, which can be smaller than the number of times it is used in the fully expanded proof). Incomplete proofs (with unknown steps) keep the references they have. The database is updated continuously; the networks are of the database at the last commit of each year from 2015 to 2025 (`2015` ... `2025`, from the GitHub repository), and of 31 October 2026 (`2026`). The networks have the following properties: - `name`: the label of the assertion (e.g. `ax-mp`, `df-an`, `id`), whose page is `https://us.metamath.org/mpeuni/<name>.html`. - `kind`: `theorem`, `axiom` (`$a |- statements other than definitions), definition (labels starting with df-) or syntax. - statement: the statement of the assertion, as Metamath symbols (e.g. |- ( ph -> ph )). - part, chapter, section: the headings of the part, chapter and section of the database in which the assertion appears (e.g. CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY, Propositional calculus); the users' mathboxes (personal sections of the contributors, with material not yet moved to the main body) are in the part SUPPLEMENTARY MATERIAL (USERS' MATHBOXES). - contributor: the contributor of the assertion, as given in its comment (usually the initials of a contributor of the list in the header of the database, e.g. NM for Norman Megill). - contributed: the date of the contribution as given in its comment, as Unix time (-1 if not given). - discouraged: whether new usage of the assertion is discouraged (as stated in its comment). - Edge count: the number of references to the assertion in the proof (as stored).

Tags

Informational Relatedness Weighted Metadata

Citation

N. Megill, D. A. Wheeler, "Metamath: A Computer Language for Mathematical Proofs." Lulu Press, Morrisville, North Carolina (2019) us.metamath.org

Upstream URL OK

https://us.metamath.org/
https://github.com/metamath/set.mm

Upstream license

CC0, https://creativecommons.org/publicdomain/zero/1.0/

Networks

Tip: click on a column header to sort the list, or hover over it for a description.

Column legend

$\left<k\right>$: Mean degree
$\sigma_k$: Standard deviation of the degrees
$\lambda_h$: Largest eigenvalue of the Hashimoto (non-backtracking) matrix
$\tau$: Random walk mixing time
$r$: Degree assortativity
$c$: Global clustering coefficient
$\oslash$: (Pseudo-) diameter
$S$: Relative size of the largest component
NPs: Node properties
EPs: Edge properties

Name	Nodes	Edges	$\left<k\right>$	$\sigma_k$	$\lambda_h$	$\tau$	$r$	$\oslash$	$S$	Kind	Mode	NPs	EPs	gt	GraphML	GML	csv
2015	29,244	803,801	27.49	289.96	364.87	6.64	-0.16	7	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	1.5 MiB	4.1 MiB	3.9 MiB	3.0 MiB
2016	30,379	849,904	27.98	298.79	373.33	6.66	-0.16	8	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	1.6 MiB	4.3 MiB	4.1 MiB	3.2 MiB
2017	31,981	916,147	28.65	310.16	388.96	6.66	-0.16	7	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	1.7 MiB	4.7 MiB	4.5 MiB	3.4 MiB
2018	34,034	987,993	29.03	322.07	402.93	6.31	-0.16	7	1.00	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	1.9 MiB	5.1 MiB	4.8 MiB	3.7 MiB
2019	36,633	1,088,443	29.71	340.00	426.38	6.27	-0.16	7	1.00	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.0 MiB	5.6 MiB	5.3 MiB	4.1 MiB
2020	40,426	1,213,085	30.01	360.37	450.94	5.78	-0.16	8	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.3 MiB	6.2 MiB	5.9 MiB	4.6 MiB
2021	42,119	1,260,493	29.93	366.76	458.05	5.88	-0.16	8	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.4 MiB	6.5 MiB	6.2 MiB	4.7 MiB
2022	43,270	1,283,652	29.67	368.88	460.24	5.86	-0.16	8	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.4 MiB	6.6 MiB	6.3 MiB	4.8 MiB
2023	44,507	1,312,934	29.50	371.27	462.75	5.95	-0.16	8	0.99	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.5 MiB	6.8 MiB	6.5 MiB	5.0 MiB
2024	46,567	1,375,967	29.55	380.33	472.39	5.91	-0.16	8	1.00	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.6 MiB	7.1 MiB	6.8 MiB	5.2 MiB
2025	49,765	1,484,326	29.83	396.19	489.57	5.91	-0.16	8	1.00	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.8 MiB	7.7 MiB	7.3 MiB	5.6 MiB
2026	51,242	1,523,526	29.73	400.39	494.56	5.91	-0.16	8	1.00	Directed	Unipartite	name kind statement part chapter section contributor contributed discouraged	count	2.9 MiB	7.9 MiB	7.5 MiB	5.8 MiB