Incidences, tilings, and fields

(joint work with P. Pylyavskyy, arXiv:2505.02229)
Incidence theorems about points and lines in the plane are at the core of projective geometry, and their automated proofs are studied in mathematical logic. One approach to such proofs, which originated from Coxeter/Greitzer’s proof of Pappus’ theorem, is multiple applications of Menelaus's theorem. Richter-Gebert, Fomin, and Pylyavskyy visualized them using triangulated surfaces. We investigate which incidence theorems can or cannot be proved in this way. We show that, in addition to triangulated surfaces, one can use simplicial complexes satisfying a certain excision property. This property holds, for instance, for the generalization of gropes that we provide. We introduce a hierarchy of classes of theorems based on the underlying topological spaces. We show that this hierarchy does not collapse over $\mathbb R$ by considering the same theorems over finite fields.

Link for connecting to the seminar: https://mian.ktalk.ru/j1xwg956wc7a
"PIN code": The number of homotopy classes of maps from the Russian word ПЁС to the Russian word ЁЖ (where a word is understood as the subset of the plane formed by its letters)