Architecture

ProofAtlas is organized into four interconnected layers. Each layer serves a single purpose and exposes a clean interface to the layers above and below.

Layer 1 · Proof layer

The Lean kernel and a small library of structural definitions on top of it. This is where mathematics lives in its primary form: propositions, proof terms, dependencies.

ProofAtlas/Combinatorial/ defines the hypergraph — directed, ordered, coloured, acyclic, connected — as a Lean 4 structure. Vertices are propositions; hyperedges are individual inference steps; the colour records the rule applied. The four structural axioms (D, O, C, A) are encoded as fields, not as auxiliary lemmas, so they hold by construction.

ProofAtlas/Metric/Axioms.lean defines the IsHypergraphMetric spec: seven fields that a candidate distance must satisfy to be a "metric on proof hypergraphs" in the sense of the paper.

Layer 2 · Translation layer

ProofAtlas/Mapping/Expr.lean is the bridge. Given any e : Lean.Expr, it produces

Lean.Expr.toHypergraph e : Hypergraph (Fin (countSubterms e)) ExprColor

with all five structural axioms machine-checked. The proof of the connected field — every non-root DFS vertex is incident to its parent compound — is the load-bearing lemma; once it is sealed, every Lean declaration in any library ships with a hypergraph for free.

Layer 3 · Compute layer

ProofAtlas/Pipeline/ runs the actual numbers. It is intentionally separate from the proof layer: Float arithmetic, no proof obligations, fully #eval-able. The dataflow is

Lean.Environment
  ↓  Environment.toIncidenceData     (DFS walk + const-sharing)
IncidenceData
  ↓  resistanceMatrix                 (Gaussian elimination)
Array (Array Float)
  ↓  hyperbolicityConstant            (4-tuple enumeration)
Float

The compute layer's only contract with the proof layer is shape: an IncidenceData represents the same combinatorial object as a Hypergraph. A future bridging lemma will pin that down formally; for now the two layers are kept on speaking terms by convention.

Layer 4 · Quality layer

Tests, linters, and CI. scripts/check_bdf_metric_instances.sh walks the metric registry and refuses to ship a metric whose IsHypergraphMetric instance theorem still contains sorry. The HypergraphGeo.Linter.MathTag linter forces every declaration to tag its docstring as Math, Eng, or Mixed, so it is always obvious which lines correspond to paper content and which are type-theoretic plumbing.

What this site documents

The pages in this section trace the four steps of the ProofAtlas project, mirroring the layer structure:

• Step 1 — the hypergraph and the Lean.Expr translation.
• Step 2 — the IsHypergraphMetric spec (outer layer) and the four metrics currently registered against it (resistance, commute time, Jensen–Shannon, diffusion).
• Step 3 — the theory developed on top: δ-hyperbolicity, spectral identities, Hausdorff and Gromov–Hausdorff.
• Step 4 — the end-to-end profile pipeline and the #atlas.* command suite.