Document Open Access Logo

Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean

Authors Garett Cunningham , Daniel Zach , Stefan Friedl

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.21.pdf
  • Filesize: 0.88 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • Lean
  • mathlib
  • simplicial complex
  • stellar subdivision
  • combinatorial topology

Metrics

Abstract

The theory of simplicial complexes is a cornerstone of topology, offering a sophisticated tool for computing invariants. We present a formalization of abstract simplicial complexes and stellar subdivisions in the Lean proof assistant. We adopt a purely combinatorial framework in order to provide a cohesive foundation for studying the theory of stellar subdivisions as seen in many contexts of combinatorial topology. In particular, we provide formalizations of morphisms between abstract simplicial complexes; several crucial constructions and operations on complexes, such as links and joins; and perform a comprehensive study of how stellar subdivisions interact with these operations. We state and prove a number of identities commonly used in the study of triangulated manifolds, such as deriving equivalences between links in an abstract simplicial complex K and in a stellar subdivision σ_s K, including results with no references in the standard literature. To our knowledge, this is the first formalization of stellar subdivisions in any proof assistant.

Cite As Get BibTex

Garett Cunningham, Daniel Zach, and Stefan Friedl. Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.21

Author Details

Garett Cunningham
  • University of Connecticut, Storrs, CT, USA
Daniel Zach
  • Universität Regensburg, Germany
Stefan Friedl
  • Universität Regensburg, Germany

Funding

The authors acknowledge support from the German-U.S. Fulbright Commission and CRC 1085 "Higher Invariants" funded by the SFB.

Supplementary Materials

References

  1. James W Alexander. The combinatorial theory of complexes. Annals of Mathematics, 31(2):292-320, 1930. Google Scholar
  2. Mirian Andrés, Laureano Lambán, Julio Rubio, and José Luis Ruiz-Reina. Formalizing simplicial topology in acl2. In Proceedings of ACL2 Workshop, volume 2007, pages 34-39, 2007. Google Scholar
  3. Jesús Aransay, Laureano Lambán, Julius Michaelis, and Julio Rubio. Formalizing alexander duality through bdds. In ISAIM, 2022. Google Scholar
  4. Jesús Aransay, Alejandro del Campo, and Julius Michaelis. Simplicial complexes and boolean functions. Archive of Formal Proofs, November 2021. Formal Proof Development. URL: https://isa-afp.org/entries/Simplicial_complexes_and_boolean_functions.html.
  5. 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, pages 521-529, 2018. URL: https://doi.org/10.1145/3209108.3209188.
  6. Benjamin A. Burton, Ryan Budney, William Pettersson, et al. Regina: Software for low-dimensional topology. http:// regina-normal. github. io/, 1999-2023. Google Scholar
  7. Mario Carneiro and Emily Riehl. Formalizing colimits in Cat. arXiv preprint, 2025. URL: https://arxiv.org/abs/2503.20704.
  8. Floris Cnossen. Simplicial sets in Lean. Bachelor thesis, 2021. Google Scholar
  9. Marshall M Cohen. A proof of newman’s theorem. Mathematical Proceedings of the Cambridge Philosophical Society, 64(4):961-963, 1968. Google Scholar
  10. Kunhong Du. On the formalization of the simplicial model of hott. Master’s thesis, Rheinischen Friedrich-Wilhelms-Universität Bonn, 2025. Google Scholar
  11. Herbert Edelsbrunner, John Harer, et al. Persistent homology - A survey. Contemporary mathematics, 453(26):257-282, 2008. Google Scholar
  12. Stefan Friedl. Topology, 2023. URL: https://www.ams.org/open-math-notes/omn-view-listing?listingId=111368.
  13. Stefan Friedl and Julian Hannes. Pachner’s theorem. In 2021-2022 MATRIX Annals, pages 777-832. Springer, 2024. Google Scholar
  14. L.C. Glaser. Geometrical Combinatorial Topology. Number v. 1 in Geometrical Combinatorial Topology. Van Nostrand Reinhold Company, 1970. Google Scholar
  15. John Harrison. A HOL light formalization of singular homology theory, 2018. URL: https://docslib.org/doc/4817357/a-hol-light-formalization-of-singular-homology-theory.
  16. Jónathan Heras, Thierry Coquand, Anders Mörtberg, and Vincent Siles. Computing persistent homology within coq/ssreflect. ACM Transactions on Computational Logic (TOCL), 14(4):1-16, 2013. URL: https://doi.org/10.1145/2528929.
  17. Jónathan Heras, Maxime Dénès, Gadea Mata, Anders Mörtberg, María Poza, and Vincent Siles. Towards a certified computation of homology groups for digital images. In Computational Topology in Image Context: 4th International Workshop, CTIC 2012, Bertinoro, Italy, May 28-30, 2012. Proceedings, pages 49-57. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30238-1_6.
  18. Jónathan Heras, Vico Pascual, and Julio Rubio. Proving with acl2 the correctness of simplicial sets in the kenzo system. In International Symposium on Logic-Based Program Synthesis and Transformation, pages 37-51. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-20551-4_3.
  19. Jónathan Heras, María Poza, Maxime Dénès, and Laurence Rideau. Incidence simplicial matrices formalized in coq/ssreflect. In International Conference on Intelligent Computer Mathematics, pages 30-44. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22673-1_3.
  20. J. F. P. Hudson. Piecewise Linear Topology. W. A. Benjamin, Inc., 1969. Google Scholar
  21. Dmitry Kozlov. Combinatorial Algebraic Topology. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71962-5.
  22. Dmitry Kozlov. Organized Collapse: An Introduction to Discrete Morse Theory, volume 207. American Mathematical Society, 2021. Google Scholar
  23. William Bernard Raymond Lickorish. Simplicial moves on complexes and manifolds. Geometry and Topology Monographs, 2(299-320):314, 1999. Google Scholar
  24. Amelia Livingston. Group cohomology in the Lean community library. In 14th International Conference on Interactive Theorem Proving (ITP 2023), pages 22:1-22:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.22.
  25. Clara Löh. Exploring Formalisation: A Primer in Human-readable Mathematics in Lean 3 with Examples from Simplicial Topology, volume 11. Springer Nature, 2022. Google Scholar
  26. Francisco-Jesus Martín-Mateos, Julio Rubio, and Jose-Luis Ruiz-Reina. Acl2 verification of simplicial degeneracy programs in the kenzo system. In International Conference on Intelligent Computer Mathematics, pages 106-121. Springer, 2009. Google Scholar
  27. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625-635, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  28. James R Munkres. Elements of Algebraic Topology. CRC Press, 2018. Google Scholar
  29. Udo Pachner. Pl homeomorphic manifolds are equivalent by elementary shellings. European journal of Combinatorics, 12(2):129-145, 1991. URL: https://doi.org/10.1016/S0195-6698(13)80080-7.
  30. Joël Riou. topcat-model-category. https://github.com/joelriou/topcat-model-category, 2024.
  31. Colin P Rourke and Brian Joseph Sanderson. Introduction to Piecewise-Linear Topology. Springer Science & Business Media, 2012. Google Scholar
  32. Julio Rubio and Francis Sergeraert. Constructive algebraic topology. Bulletin des Sciences Mathématiques, 126(5):389-412, 2002. Google Scholar
  33. Hannah Scholz. Formalisation of CW-complexes. Bachelor’s thesis, Rheinischen Friedrich-Wilhelms-Universität Bonn, 2024. Google Scholar
  34. Herbert Seifert and William Threlfall. Lehrbuch der Topologie, volume 31. American Mathematical Society, 2004. Google Scholar
  35. Francis Sergeraert. The computability problem in algebraic topology. Advances in Mathematics, 104(1):1-29, 1994. Google Scholar
  36. Francis Sergeraert. Kenzo: A symbolic software for effective homology computation, 1999. URL: https://www-fourier.univ-grenoble-alpes.fr/~sergerar/Kenzo/.
  37. RB Sher and RJ Daverman. Handbook of Geometric Topology. Elsevier, 2001. Google Scholar
  38. Edwin H Spanier. Algebraic Topology. Springer Science & Business Media, 2012. Google Scholar
  39. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 2020. ACM. URL: https://doi.org/10.1145/3372885.3373824.
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