Serre finiteness theorem formalized in Cubical Agda!

Stream: maths

[Emily Riehl]

There was a big announcement made in the HoTTEST seminar today, namely the recently-completed formalization of the Serre finiteness theorem by @Reid Barton, Owen Miller, @Axel Ljungström , @Anders Mörtberg, and @Loïc P.

[Emily Riehl]

These folks can explain better than me but let me give a bit of background. The Serre Finiteness Theorem says roughly that all of the homotopy groups of spheres are finitely presented, i.e., isomorphic to ℤʳ × ℤ/r₁ × ⋯ × ℤ/rₙ for some finite sequence of integers. @Reid Barton and Tim Campion recently discovered a proof of (a generalization of) this result in homotopy type theory that is fully constructive, i.e., which contains an algorithm that for a particular πₙ Sᵐ computes exactly this sequence of integers.

[Emily Riehl]

The formalization is in the proof assistant Cubical Agda which implements a fully constructive form of homotopy type theory called somewhat imprecisely "cubical type theory." In this system univalence is a theorem rather than an axiom. In particular, this formal system satisfies a metatheoretic property called normalization which says that a closed term (meaning in the empty context) of type ℤ is an explicit integer.

[Emily Riehl]

Now the Barton-Campion algorithm formalized by the team mentioned above only computes all homotopy groups of spheres in theory. Past history with the Brunerie number suggests it will take a lot of optimization before it can compute any homotopy groups of sphere in practice. On the other hand, the entire algorithm, plus a lot of beautiful background mathematics about CW-complexes and a new notion of stably almost finite homotopy types has now been formally verified. This is very cool!

[Floris van Doorn]

This is really cool! Congrats to the authors!