Step 3 · Theory

The theory stack ProofAtlas formalises is three layers thick. Each layer builds on the one below, and each has a dedicated page.

Layer 1 — Structure

A hypergraph (in the sense of Barkeshli–Douglas–Freedman) is directed, ordered, coloured, and acyclic. It is the combinatorial fingerprint of a CIC proof term: every Lean.Expr deterministically lowers to one.

→ Structure layer

Layer 2 — Metric

Four candidate distances are registered against the IsHypergraphMetric specification:

Distance	Page	Intuition
Resistance	Resistance	how hard is it to cut the connection?
Commute time	Commute time	random walk round-trip cost
Jensen–Shannon	Metrics overview	divergence of stationary neighbourhoods
Diffusion	Metrics overview	heat-kernel distance at scale $t$

Two are sorry-free (resistanceDist, commuteTimeDist); the other two are in progress. The Quality page explains what "certified" means and how to check it via #atlas.status.

Layer 3 — Geometry

Once a distance is an IsHypergraphMetric, all of metric geometry applies to it generically. The headline invariant is Gromov δ-hyperbolicity — a single real number that says how tree-like the proof landscape is at large scale. Two further notions, the Hausdorff distance between proof skeletons and the Gromov–Hausdorff distance between whole proof hypergraphs, sit on the same generic API.

→ Hyperbolicity

How the pieces fit

  Lean.Expr  ──Layer 1──►  Hypergraph
                              │
                              │  pick a metric:
                              ▼
                       (V, d) ──Layer 2──►  metric space
                              │
                              │  generic geometric theorems:
                              ▼
                  δ, Hausdorff, GH ──Layer 3──►  proof landscape

Every theorem in Layer 3 quantifies over an arbitrary IsHypergraphMetric, so swapping resistance for Jensen–Shannon doesn't invalidate any result. The four metric definitions are interchangeable inputs into the same generic theory.

References

[BDF26] Barkeshli, Douglas, Freedman, Artificial Intelligence and the Structure of Mathematics, arXiv:2604.06107, 2026. §§5–7.