Formalization of homotopy theory in Lean

Abstract: Model categories structures introduced by Quillen are a framework in order to do homotopy theory. In this talk, I will outline my formalization of the model category structures on the categories of topological spaces and simplicial sets.

logic in computer sciencemathematical softwarealgebraic topology

Audience: researchers in the discipline

( slides | video )

Lean Together 2026