Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach
Computational Geometry
2022-01-04 v1 Mathematical Software
Symbolic Computation
Abstract
Several tools have been developed to enhance automation of theorem proving in the 2D plane. However, in 3D, only a few approaches have been studied, and to our knowledge, nothing has been done in higher dimensions. In this paper, we present a few examples of incidence geometry theorems in dimensions 3, 4, and 5. We then prove them with the help of a combinatorial prover based on matroid theory applied to geometry.
Cite
@article{arxiv.2201.00539,
title = {Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach},
author = {Pascal Schreck and Nicolas Magaud and David Braun},
journal= {arXiv preprint arXiv:2201.00539},
year = {2022}
}
Comments
In Proceedings ADG 2021, arXiv:2112.14770