Lean is a platform for writing proofs in a formal language that can be machine-checked for correctness. Mathlib is a library that contains a vast collection of mathematical theorems and definitions, including topological spaces and manifolds.

Perhaps in the coming years, math papers will be expected to include formal proofs of their correctness. As a glimpse into this possible future, this talk includes a demonstration of Lean and will focus on examples drawn from topology. Participants interested in learning more will receive practical next steps.