Formalized Spectral Sequences in Homotopy Type Theory II

Spectral sequences form a powerful tool for computing algebraic properties such as homotopy groups, homology groups and cohomology groups of spaces in algebraic topology. In this second talk I will talk about the cohomological Atiyah-Hirzebruch and Serre spectral sequences in the logic of homotopy type theory. This has been formalized in Lean, a new proof assistant which supports reasoning in homotopy type theory.