Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean
2026-07-11 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors formalized a key part of topology called abstract simplicial complexes using the Lean proof assistant, a tool for checking mathematical proofs. They focused on a process called stellar subdivision, which breaks down shapes into smaller pieces, and studied how this interacts with other operations on these complexes. Their work includes proving known and some previously unreferenced results about these subdivisions. This is the first time stellar subdivisions have been fully formalized in any proof assistant.
abstract simplicial complexstellar subdivisiontopologyLean proof assistantmorphismslinksjoinstriangulated manifoldscombinatorial topology
Authors
Garett Cunningham, Daniel Zach, Stefan Friedl
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.