Imagine you want to break a complicated shape into simple triangular pieces, like cutting a 3D object into tetrahedra. Mathematicians use a framework called simplicial complexes to make this idea rigorous: you build shapes by gluing together points, line segments, triangles, tetrahedra, and their higher-dimensional cousins in a consistent way. A stellar subdivision is a specific operation that lets you refine this triangulation by introducing a new point and retriangulating a piece of the complex around it. These tools are fundamental to topology, the branch of mathematics concerned with the properties of shapes that survive stretching and bending. This paper takes these classical ideas and encodes them inside Lean, a computer-based proof assistant that can mechanically verify every logical step of a mathematical argument.
The specific contribution is a fully verified library of definitions, constructions, and theorems about simplicial complexes and stellar subdivisions. The authors formalize not just the objects themselves but also the maps between them, and important operations like links (roughly, the neighborhood structure around a piece of the complex) and joins (a way of combining two complexes into a higher-dimensional one). They then prove a comprehensive collection of identities describing how stellar subdivisions interact with these operations, including some results that apparently had not been written down explicitly in the existing literature before.
Why does this matter? Simplicial complexes and triangulations are used across mathematics and computer science, from computing topological invariants of data to verifying geometric algorithms. When proofs in this area get long and combinatorially intricate, errors can slip through unnoticed in human-written work. By formalizing these foundations in a proof assistant, the authors create a trustworthy, reusable base that future researchers can build on with confidence. They also demonstrate that proof assistants are mature enough to handle non-trivial combinatorial topology, which is an encouraging sign for the broader project of making mathematics more reliably checkable by machines.