Formalizations, in Lean 4 and Mathlib, of results from my research on graphs, networks, and the modulus of families of objects.
This is a working project. results are added incrementally, and the
blueprint tracks what's genuinely proved versus proved with sorry.
| 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.
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.