A Computer Formalisation of the Serre Finiteness Theorem

Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear at first glance to be almost completely random -an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1951, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT) -an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented -and constructively so. Prior to this proof, only low-dimensional homotopy groups of spheres had been computed in HoTT. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion's proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavour of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.