Document Open Access Logo

A Computer Formalisation of the Serre Finiteness Theorem

Authors Reid Barton , Axel Ljungström , Owen Milner , Anders Mörtberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.16.pdf
  • Filesize: 1.3 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Homotopy type theory
  • synthetic homotopy theory
  • formalisation of mathematics
  • constructive mathematics

Metrics

Abstract

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.

Cite As Get BibTex

Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.16

Author Details

Reid Barton
  • Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, Sweden
Axel Ljungström
  • School of Computer Science, University of Nottingham, UK
Owen Milner
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
Anders Mörtberg
  • Department of Mathematics, Stockholm University, Sweden

Funding

  • Barton, Reid: ForCUTT project, ERC advanced grant 101053291.
  • Ljungström, Axel: Knut & Alice Wallenberg Foundation’s Program for Mathematics.
  • Milner, Owen: This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey.

Acknowledgements

We wish to thank Loïc Pujet, who has followed this project closely, for many fruitful meetings and discussions. The third author would also like to thank Mathieu Anel for helpful guidance when he was formalising the proof of Proposition 34. Finally, we would like to thank our anonymous reviewers for their careful readings and useful remarks.

Supplementary Materials

References

  1. Mathieu Anel, Georg. Biedermann, Eric. Finster, and André Joyal. A Generalized Blakers–Massey Theorem. Journal of Topology, 13:1521-1553, March 2020. URL: https://doi.org/10.1112/topo.12163.
  2. Reid Barton and Tim Campion. A synthetic approach to finite presentability of homotopy groups. Preprint, 2026. URL: https://github.com/CMU-HoTT/serre-finiteness/blob/main/Paper/barton-campion.pdf.
  3. Reid Barton, Axel Ljungström, Owen Milner, and Anders Mörtberg. A Computer Formalisation of the Serre Finiteness Theorem (accompanying formalisation). Software, ForCUTT project, ERC advanced grant 101053291, Knut & Alice Wallenberg Foundation’s Program for Mathematics, This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0009, PI Steve Awodey, (visited on 2026-06-29). URL: https://github.com/CMU-HoTT/serre-finiteness
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26876
  4. Edgar H. Brown. Finite Computability of Postnikov Complexes. Annals of Mathematics, 65(1):1-20, 1957. URL: http://www.jstor.org/stable/1969664.
  5. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université Nice Sophia Antipolis, 2016. URL: https://arxiv.org/abs/1606.05916.
  6. Ulrik Buchholtz and Kuen-Bang Hou Favonia. Cellular Cohomology in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 521-529, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209188.
  7. Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles. Formalized linear algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:7)2016.
  8. Evan Cavallo and Robert Harper. Higher Inductive Types in Cubical Computational Type Theory. Proceedings of the ACM on Programming Languages, 3(POPL):1:1-1:27, January 2019. URL: https://doi.org/10.1145/3290314.
  9. J. Daniel Christensen and Luis Scoccola. The Hurewicz theorem in Homotopy Type Theory, 2020. Preprint. URL: https://arxiv.org/abs/2007.05833.
  10. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  11. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  12. Samuel Eilenberg and Norman E. Steenrod. Axiomatic Approach to Homology Theory. Proceedings of the National Academy of Sciences, 31(4):117-120, 1945. URL: https://doi.org/10.1073/pnas.31.4.117.
  13. Tudor Ganea. A generalization of the homology and homotopy suspension. Commentarii Mathematici Helvetici, 39(1):295-322, December 1964. URL: https://doi.org/10.1007/BF02566956.
  14. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002. URL: https://pi.math.cornell.edu/~hatcher/AT/AT.pdf.
  15. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933575.2934545.
  16. Simon Huber. Canonicity for Cubical Type Theory. Journal of Automated Reasoning, June 2018. URL: https://doi.org/10.1007/s10817-018-9469-1.
  17. Daniel C. Isaksen, Guozhen Wang, and Zhouli Xu. Stable homotopy groups of spheres: from dimension 0 to 90. Publications mathématiques de l'IHÉS, 137(1):107-243, June 2023. URL: https://doi.org/10.1007/s10240-023-00139-1.
  18. Tom Jack and Axel Ljungström. Yet another homotopy group, yet another Brunerie number, 2025. Extended abstract at Types 2025. URL: https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper66.pdf.
  19. R.-J. Kang. Formalization of the existence of the Smith normal form, 2022. URL: https://github.com/agda/cubical/blob/master/Cubical/Algebra/IntegerMatrix/Smith/Normalization.agda.
  20. Stanley O. Kochman. Stable homotopy groups of spheres. Lecture Notes in Mathematics. Springer, Berlin, Germany, 1990 edition, April 1990. Google Scholar
  21. Daniel R. Licata and Guillaume Brunerie. π_n(Sⁿ) in homotopy type theory. In Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, pages 1-16, Berlin, Heidelberg, 2013. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-03545-1_1.
  22. Daniel R. Licata and Eric Finster. Eilenberg-MacLane Spaces in Homotopy Type Theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603153.
  23. Daniel R. Licata and Michael Shulman. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 223-232, Washington, DC, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2013.28.
  24. Axel Ljungström and Anders Mörtberg. Formalizing π₄(S³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175833.
  25. Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. Preprint, 2025. URL: https://aljungstrom.github.io/files/cellular2025.pdf.
  26. Axel Ljungström and Anders Mörtberg. Computational synthetic cohomology theory in homotopy type theory. Mathematical Structures in Computer Science, 35:e16, 2025. URL: https://doi.org/10.1017/S0960129525000131.
  27. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. URL: https://doi.org/10.1017/S030500411900015X.
  28. Owen Milner. Connected Covers in Cubical Agda. Slides from the Workshop on Homotopy Type Theory/Univalent Foundations (HoTT/UF 2024), 2024. URL: https://hott-uf.github.io/2024/slides/Milner.pdf.
  29. Semen Sergeevich Podkorytov. An Alternative Proof of a Weak Form of Serre’s Theorem. Journal of Mathematical Sciences, 110(4):2875-2881, July 2002. URL: https://doi.org/10.1023/A:1015370800473.
  30. Julio Rubio and Francis Sergeraert. Constructive algebraic topology. Bulletin des Sciences Mathématiques, 126(5):389-412, 2002. URL: https://doi.org/10.1016/S0007-4497(02)01119-3.
  31. Jean-Pierre Serre. Homologie singulière des espaces fibrès. Annals of Mathematics, 54(3):425-505, 1951. URL: http://www.jstor.org/stable/1969485.
  32. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential colimits in homotopy type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 845-858, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3373718.3394801.
  33. The Agda Development Team. The Agda Programming Language, 2023. URL: http://wiki.portal.chalmers.se/agda/.
  34. The Rocq Development Team. The Rocq Proof Assistant, 2025. URL: https://rocq-prover.org/.
  35. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  36. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Journal of Functional Programming, 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  37. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, February 2010. Notes from a talk at Carnegie Mellon University. URL: http://www.math.ias.edu/vladimir/files/CMU_talk.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact