Command Reference

The #atlas.* commands run end-to-end inside Lean: they resolve an identifier, walk its proof term into a hypergraph, run the chosen computation, and render the result in the VS Code infoview.

Multi-identifier commands glue the proof terms via const-sharing before computing; the per-input root vertices end up in HypergraphReport.roots.

#atlas.graph

Draw the hypergraph of one or more declarations.

#atlas.graph Nat.add_zero
#atlas.graph Nat.add_zero Nat.add_comm  -- shared constants merged

Output: Interactive force-directed graph in VS Code infoview. Vertices = sub-expressions. Hyperedges = constructor applications. Colors: app (red), lam (green), forallE (orange), letE (purple), mdata (gray), proj (brown).

What this measures. Renders the hypergraph of one or more declarations. Vertices are sub-expressions. Hyperedges are constructor applications (app, lam, forallE, letE, ...), colored by type.

→ Theory: Structure layer — what a hypergraph is, why these four properties capture CIC.

#atlas.resistance

Compute the resistance distance between two declarations.

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

The two proof terms are glued into one hypergraph via const-sharing; the result is the effective resistance between their root vertices.

What this measures. How well-connected two declarations are through their shared constant network. Two proof terms are glued into a single graph via const-sharing; the resistance distance between their root vertices reflects how much shared infrastructure links them. Close = tightly connected through common constants. Far = few shared paths.

→ Theory: Resistance distance — spectral formula, conductance schedule, Rayleigh monotonicity.

#atlas.hausdorff.resistance

Hausdorff distance between two groups of declarations under the resistance metric. The | token separates the two groups.

#atlas.hausdorff.resistance Nat.add_zero | Nat.add_comm Nat.succ_eq_add_one
-- Hausdorff(resistance, {Nat.add_zero}, {Nat.add_comm, Nat.succ_eq_add_one}) = 1.752143

Every declaration on either side is glued into one hypergraph via const-sharing; the resistance matrix is computed once on the combined graph; the Hausdorff distance is taken over the union of subtree vertex sets per group (not the singleton root vertices).

What this measures. How structurally similar two groups of proof terms are. For each sub-expression in group A, finds the closest sub-expression in group B (by resistance distance), then takes the worst case. A small Hausdorff distance means every part of one proof has a structural counterpart in the other.

→ Theory: Resistance distance — Hausdorff lifts any base metric to sets, inheriting symmetry and triangle inequality from Mathlib.

#atlas.delta

Compute the Gromov δ-hyperbolicity constant.

#atlas.delta Nat.add_zero Nat.add_comm Nat.succ_eq_add_one
-- δ = 0.238369, diam = 3.213827, δ/diam = 0.074170

What this measures. How tree-like the proof structure is at large scale. A small δ/diam ratio means the shared constant network has a hierarchical, tree-like backbone. A large ratio means it has significant non-tree shortcuts.

→ Theory: δ-hyperbolicity — four-point condition, thin triangles, δ/diam ratio.

#atlas.profile

Comprehensive report: graph + vertices/edges + resistance matrix + δ.

#atlas.profile Nat.add_zero

What this measures. Full geometric report: vertex/edge counts, color distribution, resistance diameter, mean resistance, δ-hyperbolicity, δ/diam ratio.

→ Theory: Overview — the three-layer pipeline from structure to geometry.

#atlas.graph.ns

Decl-level companion to #atlas.graph: build the co-reference graph of an entire namespace. Vertices = declarations, hyperedges = maximal application spines inside each declaration's proof body.

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

What this measures. The shape of a library, not a single proof: which declarations cite which, and how dense the co-reference network is. Vertex colour by declaration kind (theorem / def / instance / axiom / opaque).

The first .ns call on a namespace pays a one-time cost (~2 s for ~200 decls) to build the decl-graph + resistance matrix; subsequent .resistance.ns and .delta.ns on the same namespace are cache hits.

#atlas.resistance.ns

Effective resistance between two declarations on the decl-level graph of a namespace.

#atlas.resistance.ns ProofAtlas.Pipeline geometricProfile geometricProfileOfExprs
-- R(...geometricProfile, ...geometricProfileOfExprs) = 0.331177
--   [same component (#2/24)]

What this measures. How close two declarations are in the co-reference structure of their namespace. Short names auto-qualify against the namespace argument. The output also reports whether the two ends sit in the same weakly-connected component — a different- component result is ε⁻¹-scale noise (the regularised pseudoinverse).

→ Theory: same as #atlas.resistance; the metric is the same, the graph it's computed on is different (decls vs subterms).

#atlas.delta.ns

Gromov δ-hyperbolicity of the decl-level graph of a namespace, restricted to the largest connected component (the full graph is typically disconnected).

#atlas.delta.ns ProofAtlas.Pipeline
-- δ      = 0.090615
--    diam   = 3.839542
--    δ/diam = 0.023600
--    [24 components — δ/diam restricted to largest (215 verts)]

What this measures. Large-scale tree-likeness of the namespace's co-reference network. A small δ/diam (under ~0.1) means the library's decl graph is hierarchical; larger ratios mean it has significant non-tree shortcuts.

First call on a namespace is the C(n,4) δ enumeration (tens of seconds for ~200 verts); subsequent calls are cache hits.

→ Theory: δ-hyperbolicity.

#atlas.status

Check whether a metric has a verified IsHypergraphMetric instance.

#atlas.status resistanceDist      -- ✓ certified
#atlas.status commuteTimeDist     -- ✓ certified
#atlas.status jsDist              -- ⚠ in progress

What this measures. Whether a metric's IsHypergraphMetric instance is sorry-free. Reports ✓ (certified), ⚠ (in progress, transitively uses sorry), or ✗ (not registered).

→ Theory: Quality (IsHypergraphMetric) — the seven-check certificate every registered metric must satisfy.