ProofAtlas

Tutorial — your first ProofAtlas profile

This walk-through gets you from a blank Lean 4 project to a working #atlas.profile in about five minutes. You will need:

  • A working Lean 4 toolchain (elan + lake).
  • VS Code with the Lean 4 extension (for the interactive InfoView, which is where most #atlas.* output renders).

1. Add ProofAtlas to your lakefile.toml

In your project's lakefile.toml:

[[require]]
name = "proofatlas"
git = "https://github.com/MathNetwork/ProofAtlas"
rev = "main"
subDir = "lean"

Your lean-toolchain must match ProofAtlas's. Check lean/lean-toolchain in the repo for the current value (currently leanprover/lean4:v4.30.0-rc2).

Then:

lake update
lake build

lake update fetches ProofAtlas and Mathlib; lake build compiles them. The first build downloads the Mathlib cache and takes a few minutes; subsequent builds are incremental.

For a local checkout instead of the git remote, swap the git/rev lines for path = "/absolute/path/to/hypergraph-geo/lean".

2. Try the commands in a .lean file

Open any .lean file in your project, side-by-side with the Lean InfoView pane (in VS Code: Cmd+Shift+P → Lean 4: Infoview: Toggle Infoview). Type:

import ProofAtlas

#atlas.graph Nat.add_zero

The InfoView should show an interactive force-directed graph: small open circles for subterm vertices, coloured rectangles for hyperedges (constructor applications), with two range sliders for tuning the d3-force simulation. Hover any node for a tooltip; drag to pin.

Next, ask for the full report:

#atlas.profile Nat.add_zero

You'll see the same graph plus a text summary:

Hypergraph Report
  vertices    7
  edges       3  [app=3]
  diameter    1.333
  mean dist   1.000
  δ           0.000
  δ / diam    0.000

δ = 0 means the proof is exactly tree-like at this scale (no non-trivial four-point deviation).

3. Glue two declarations and measure the resistance between them

#atlas.resistance Nat.add_zero Nat.add_comm
-- R(Nat.add_zero, Nat.add_comm) = 1.179960

The two proof terms are merged into a single hypergraph via const-sharing: every .const Name reference (Nat, HAdd.hAdd, Eq, ...) appears as one shared vertex. The result is the effective electrical resistance between the two root vertices on that combined graph.

Read it as "how independent are these two propositions, given the shared infrastructure they both rely on?" Smaller = more shared backbone, more entangled. Larger = more independent.

To see the same glue visually:

#atlas.graph Nat.add_zero Nat.add_comm

4. Try the decl-level view

The commands above work at the subterm level. For a wider lens — vertices = whole declarations, edges = co-references between them — use the .ns variants:

#atlas.graph.ns ProofAtlas.Pipeline
-- Decl-level hypergraph (ProofAtlas.Pipeline): 240 vertices, 1100 hyperedges

The first call to any .ns command builds a cache of the namespace's decl-graph (~2 seconds for ~200 declarations); subsequent .resistance.ns and .delta.ns queries reuse it.

5. Export from the CLI (no editor required)

For shell pipelines, snapshots, or any non-interactive use, run:

cd lean
lake exe atlas-export Nat.add_zero

This prints a JSON document with the incidence data, resistance matrix, and δ. A formally-versioned schema is on the roadmap.

Next steps

If something goes wrong

  • unknown identifier '#atlas.graph' — import ProofAtlas is missing, or lake build hasn't finished.
  • InfoView blank where a widget should be — the widget didn't load; check the VS Code Output panel for the Lean server log.
  • Mathlib cache miss on lake build — re-run lake exe cache get then lake build.
  • A .ns command takes 30+ seconds the first time you run it on a large namespace — that's the C(n,4) δ-enumeration; subsequent calls are cached.
  • Anything else: open an issue with the bug report template.