Formalizations, in Lean 4 and Mathlib,
of results from research on graphs, networks, and the modulus of families of objects. This is a
working project — results are added incrementally, and the blueprint below tracks
what’s genuinely proved versus proved with sorry.
Papers
| Paper | Status | Lean source |
|---|---|---|
| Fairest Edge Usage and Minimum Expected Overlap for Random Spanning Trees (Albin, Clemens, Hoare, Poggi-Corradini, Sit, Tymochko, 2021) | 🚧 just started | LeanModulus/Papers/FairestEdgeUsage |
More papers will be added here as they’re formalized.
Dependency graph
Each node below is a definition or theorem from the blueprint; colors show what’s formalized,
what’s ready to formalize next, and what’s still blocked. Click a node to see its statement. Check the
legend for color coding. You can also view the full-page version.
This graph, the blueprint pages it’s embedded in, and the proved/sorry tracking throughout this
site are all generated by leanblueprint.
Resources
- Zulip chat for Lean for coordination
- Design notes — encoding choices, deviations from the paper, open TODOs
- leanblueprint — the tool that generates the blueprint and dependency graph on this site
Why formalize this
I’m moving toward including Lean theorem proving in my courses and my research workflow. Formalizing results from my recent papers is a way for me to practice writing Lean proofs for real mathematical content rather than textbook exercises. It also gives me a chance to explore the various AI tools for Lean, and to see how well they can help with real research-level mathematics.