This page tracks the progress of the Lean 4/Mathlib formalization of some of my research on graphs, networks, and the modulus of families of objects.

Papers

See the papers table in the README for the current list of papers and their formalization status.

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

See the README on GitHub for the motivation behind this project.