This repo contains Lean 4/Mathlib formalization of some of my research on graphs, networks, and the modulus of families of objects. A brief introduction to modulus and some associated code can be found in my discrete-modulus repo.
You can also find a more complete coverage of the theory in my book with Pietro Poggi-Corradini:
Albin, N., & Poggi-Corradini, P. (2025). Mathematics of Networks: Modulus Theory and Convex Optimization (1st ed.). Chapman and Hall/CRC. https://doi.org/10.1201/9781003024866
This is a working project. Results and the upcoming plan are tracked in the blueprint, tracks what's defined, stated, and proved.
| 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.
Building toward the goals of the papers, the following shared infrastructure is
formalized in the Common folder:
- Multigraphs — forests, spanning trees, connected components
(
Multigraph.lean) - Graphic matroid — forests as the independent sets of the cycle matroid
(
GraphicMatroid.lean) - Modulus / families of objects — densities, admissible sets, Fulkerson duals
(
FamilyOfObjects.lean,ToReal.lean) - Convex analysis for duality — extreme points, Krein-Milman-adjacent lemmas
(
ExtremePoints.lean) SimpleGraphconnectivity facts (SimpleGraph.lean)
LeanModulus/
Papers/
FairestEdgeUsage/ -- one folder per paper, files roughly track paper section numbers
Common/ -- shared definitions/lemmas reused across papers (multigraphs, etc.)
blueprint/ -- LaTeX source mapping paper statements to Lean declarations
docs/ -- design notes: encoding choices, deviations from the paper, open TODOs
Each paper's Lean files cite the definition/theorem numbers they formalize, so you can read the
Lean code side-by-side with the paper. See docs/ for translation notes — places where the
Lean formalization had to make a choice the paper didn't have to (e.g. how multigraphs are encoded).
This project uses Lake and depends on Mathlib. With elan installed:
lake exe cache get # fetch prebuilt Mathlib .olean files (much faster than building from source)
lake buildA devcontainer is included and does this automatically. Open the repo in VS Code and choose "Reopen in Container," or use GitHub Codespaces.
This project uses leanblueprint to maintain a
human-readable correspondence between the paper's statements and the Lean formalization, with a
dependency graph and a live count of completed vs. sorry-proved results. It is
browsable at https://nathan-albin.com/lean-modulus/.
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.