Formalisation of CW complexes

Abstract: CW complexes are a class of topological spaces that are of particular importance in algebraic topology. Intuitively, they are the result of glueing continuous images of discs together along their boundaries. My talk will concern the classical way of defining them, close to Whitehead’s original definition. I will first discuss the definition and a particular challenge with typeclass inference that we faced when implementing it in Lean. Afterwards, I will report on the current status of CW complexes in Lean and lastly, I will give a glimpse of the mathematically most interesting part of the project: the product of CW complexes. All the work that I will be presenting was done together with and supervised by Prof. Floris van Doorn.

logic in computer sciencemathematical softwarealgebraic topology

Audience: researchers in the discipline

( slides | video )

Lean Together 2026