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.
target
chosen chain
Stable-source checked theorem
Alpha-only checked theorem; historical candidate-factory source
declared but not cited in tactic body
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