ProofGraph
Network science and spectral graph theory applied to formalized mathematics.
ProofGraph extracts declaration-level dependency graphs from Lean 4 projects, computes proof-theoretic properties, runs structural and spectral analysis, and exposes everything through APIs and an MCP server.
About the Project
The core insight comes from the Curry-Howard-Lambek correspondence: proofs are programs, propositions are types, and logical systems are categories.
A formalized mathematics library like Lean’s Mathlib — with 250,000+ theorems and 120,000+ definitions — is a complex network whose structure can be studied empirically.
ProofGraph makes this structure visible and queryable.
Research Areas
- Dependency graph extraction from Lean 4 formalized libraries
- Spectral graph theory applied to proof networks
- Network science metrics — centrality, modularity, community detection
- Proof-theoretic properties computed at the declaration level
- API and MCP server for programmatic access to graph data