Announcing ProofGraph

We’re kicking off development of ProofGraph, a research project and open-source platform that will bring network science and spectral graph theory to formalized mathematics.

The idea

Formalized mathematics libraries like Lean’s Mathlib — with over 250,000 theorems and 120,000 definitions — form vast, intricate dependency networks. ProofGraph aims to make this structure visible and queryable.

The project builds on a foundational insight from the Curry-Howard-Lambek correspondence: proofs are programs, propositions are types, and logical systems are categories. This means a formalized library isn’t just a collection of theorems — it’s a complex network whose structure can be studied empirically.

What we’re building

ProofGraph will extract declaration-level dependency graphs from Lean 4 projects and provide:

• Structural analysis — centrality, modularity, and community detection across proof networks
• Spectral graph theory — eigenvalue analysis revealing deep structural properties
• Proof-theoretic metrics — computed at the declaration level
• APIs and an MCP server — for programmatic access to graph data

Follow along

Development is just getting started. The project is open source — check out the GitHub repository. We’ll be sharing progress updates, early results, and research findings here as the project takes shape. Stay tuned.