Formalized Spectral Sequences in Homotopy Type Theory II

Thursday, September 21, 2017 - 12:00
427 Thackeray Hall
Speaker Information
Floris van Doorn
Carnegie Mellon University

Abstract or Additional Information

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.