Algebraic Topology in Lean

In this repo, we formalise some basic definitions of in Algebraic Topology in Lean.

Things that have been formalised

• Definition of the Fundamental Group
• Simply connected spaces
• Contractible spaces
  • Contractible spaces are simply connected

TODOs?

• The Fundamental Group of the Circle
• Brouwer's Fixed Point Theorem
• Any convex subset of a real vector space is contractible