Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach

TL;DR

This paper extends automated theorem proving in incidence geometry from 2D to higher dimensions (3D, 4D, 5D) using a combinatorial approach based on matroid theory, showcasing initial results in these complex spaces.

Contribution

It introduces a novel combinatorial prover for higher-dimensional incidence geometry, filling a gap in automated theorem proving beyond 2D.

Findings

Proved incidence theorems in 3D, 4D, and 5D.

Demonstrated the applicability of matroid theory in higher-dimensional geometry.

Extended automation tools to complex geometric spaces.

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.