The first goal is to prove that the categories of Boolean algebras and of profinite spaces are dually equivalent. A "blueprint" of the proof is available here.
- The Lean programming language and theorem prover
- Mathlib: a library of formalized mathematics
- leanblueprint: LaTeX package for making the blueprint.