Alfred Tarski developed a system of geometry that avoids treating points as fundamental building blocks. Instead, it starts with solid regions, like balls in space, and reconstructs point-like objects from nested families of shrinking spheres. The idea is philosophically attractive because we never actually perceive or measure perfect geometric points, only regions with some extent. The paper works within this tradition, using a logical framework originally due to the philosopher Stanislaw Lesniewski, and carries out the entire formal development inside Coq, a computer proof assistant that checks every logical step automatically.
The central challenge the authors tackle is topological: once you have reconstructed something like points from these nested ball families, can you build a proper topology on them? In standard mathematics, topology is usually defined directly on sets of points using a closure operator, which tells you which limit points need to be added to a set to make it complete. The authors introduce what they call point-class topology, where a reconstructed point is treated as an equivalence class of ball representatives that all converge to the same location. They then carefully define what it means for a collection of such point-classes to be open or closed, drawing the neighborhood structure from the underlying regional geometry rather than importing it from outside.
The main result is a Coq-verified proof that their closure operator satisfies the four Kuratowski axioms, which are the standard conditions any well-behaved topological closure must meet. These require, roughly, that closing a set twice gives the same result as closing it once, that closure only adds points and never removes them, that the closure of a union equals the union of the closures, and that the empty set stays empty. The authors also define topological boundaries in this setting. The significance is that they have demonstrated a rigorous, machine-checked path from a point-free regional geometry all the way up to a genuine topology, without ever having to treat the reconstructed points as fully real mereological objects in their base system.