This repository contains a completely formalized proof of the Whitehead theorem using the Lean 4 theorem prorver.

Most of my formalization directly deals with topological spaces; Joël Riou (@joelriou)'s formalization uses model categories, which is more algebraic and combinatorial, to neatly give the Whitehead theorem as a corollary.

Thanks to @dwarn and the reviewers (@joelriou, @YaelDillies, @fpvandoorn, @kmill, ...) who helped with the formal definition of CW-complexes. Also, @linlib used to have ideas for proving several variations of the Whitehead theorem, in addition to the one proved here.