Explore a proof

lein explore writes the Proof Explorer: a page you open from disk that shows what was checked. It draws the dependency graph, the proof trees, each theorem’s axiom closure, and example values that the kernel computes for natural-number and non-negative-rational equations. Nothing on the page is drawn by hand: every declaration was added by the kernel, and every statement is printed from the kernel term.

You need a clone at v1.5.5 (Install). The first example uses /tmp/add-left.edn, the bundle from Share and check a bundle.

Explore a bundle

lein explore /tmp/add-left.edn /tmp/explore-bundle

wrote /tmp/explore-bundle/index.html and data.json: 66 declarations, 1 roots, 15 with kernel-computed examples, 0 Lean badges, 0 loop badges
claim nnrat/at-most-add-left checked

About 6 seconds. The bundle is replayed as lein verify --bundle replays it before anything is drawn, so a bundle that does not check gives no page. Open /tmp/explore-bundle/index.html in a browser. The data is inline, and the graph libraries load from pinned URLs; add --offline to put them in the file too.

Explore a theorem in a checkpoint

Name the theorems to start from with --roots:

lein explore artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz /tmp/explore-ck --roots decision/finite-nnrat-argmax-dominates

wrote /tmp/explore-ck/index.html and data.json: 73 declarations, 1 roots, 1 with kernel-computed examples, 0 Lean badges, 0 loop badges

The page holds the root and everything it depends on. The theorem from Check your first proof needs 73 declarations.

Next

• Check an LP certificate: the other page for auditors.
• Commands: every lein explore option.