DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.21

Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean

Authors: Garett Cunningham, Daniel Zach, and Stefan Friedl

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{cunningham_et_al:LIPIcs.ITP.2026.21,
  author =	{Cunningham, Garett and Zach, Daniel and Friedl, Stefan},
  title =	{{Formalizing Abstract Simplicial Complexes \& Stellar Subdivisions in Lean}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{21:1--21:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.21},
  URN =		{urn:nbn:de:0030-drops-269956},
  doi =		{10.4230/LIPIcs.ITP.2026.21},
  annote =	{Keywords: Lean, mathlib, simplicial complex, stellar subdivision, combinatorial topology}
}

Search Results

Documents authored by Zach, Daniel

Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean

Abstract

Cite as

Thanks for your feedback!

Could not send message