The actual computation

The previous two talks have covered why we want to compute the descent spectral sequence for Tmf, the definition of the synthetic spectrum Smf, and seen an array of tools to work with synthetic spectra. In this talk, the rubber hits the road and we use detection methods, synthetic generalisations of the Leibniz rule and Moss' convergence theorem, and a truncated version of the Burklund--Hahn--Senger omnibus theorem to fully calculate this spectral sequence. This finally gives all the details to this computation, which was started around 30 years ago by Hopkins and Mahowald.