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.

Ссылка для подключения: https://mian.ktalk.ru/j1xwg956wc7a
PIN-код: Число гомотопических классов отображений из слова ПЁС в слово ЁЖ (где под словом понимается изображаемое его буквенной записью подмножество плоскости)