ProofAtlas

Goal

Infrastructure for anyone who wants to interpret the structure of their formalization project.

Formal mathematics produces vast amounts of proof data, yet we lack systematic tools to answer: What does the knowledge structure of mathematics look like? What is the “distance” between two theorems? Which parts of mathematics are tightly interwoven, and which can stand alone?

ProofAtlas aims to answer these questions. The approach has four steps:

1. Define the structure. Precisely define the intrinsic structure of formal proofs — how propositions depend on each other, how inference rules act, how knowledge is organized.
2. Define geometry and topology. Define verified metrics on this structure, turning the discrete proof structure into computable geometric and topological objects.
3. Develop the theory. Prove properties of these structural objects, establishing a theory of topology, metric geometry, and information theory for formal mathematics.
4. Interpret the structure. Use this theory to reveal the intrinsic structure of mathematics, generating interpretable geometric profiles end-to-end.

The entire pipeline is implemented in Lean 4, end-to-end verified from Lean.Expr to geometric profile.

Live Demo

A loop of #atlas.* commands as they appear in VS Code. Drop import ProofAtlas into any Lean 4 file and the InfoView lights up like this — every command glues the chosen proofs into a single hypergraph via const-sharing.