{"id":"arxiv/2607.10216","url":"https://arxiv.org/abs/2607.10216","tags":["cs.LO","math.AT"],"score":0,"title":"Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean","domain":"cs.LO","source":"arxiv","authors":["Garett Cunningham","Daniel Zach","Stefan Friedl"],"reviews":0,"subject":"cs.LO","summary":"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;…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-11","reactions":{}}