https://github.com/leanprover-community/mathlib4

---

Organized by Steven Clontz and Jim Fowler, this workshop is aimed at introducing students and researchers in topology to the process of formalizing topological results using the Lean theorem prover and mathlib library of formalized mathematics.

Participants are encouraged to bring a personal laptop to participate in this workshop. No software is required other than a modern web browser, and this workshop should be accessible to anyone who has completed a year of graduate-level topology.

Any SumTopo 2025 participant (in-person or virtual) can register for this workshop at this link at no additional cost.