Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Choose a path
The sparse view suppresses arrows visually only: exact direct relations remain in the details panel and graph data. Large views use compact clickable theorem marks. A theorem root has no theorem prerequisites; it is not an axiom.
Shown arrows run from prerequisite to dependent. Click a node or compact mark to make it the target; use its ↗ link, when shown, or the details-panel proof link to open the formal proof. Drag the background to pan. Use the buttons or Control/Command + wheel to zoom.
Text alternative
Ordered premise chain
The same selected route is listed here as ordinary links.
- PA language, arithmetic axioms, and proof rules foundations prelude; not a theorem node