Interactive proof map

The complete Bertrand proof

Explore every dependency of bertrand_strict, from native arithmetic foundations through the central-binomial argument and finite covering.

Choose a path

The complete cone contains all 544 theorem nodes. Focused arrows keep the initial view readable; choose all arrows for the literal 1,917-edge graph.

Layered dependency graph

Loading theorem graph…

Loading theorem graph…

Arrows run from prerequisite to dependent. Click a mark to select it, use the proof link for the exact statement and tactic body, drag to pan, and zoom with the controls.

target chosen chain checked-use body-checked declared edge

Text alternative

Ordered premise chain

  1. Loading path…