We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a combinatorial approach based on the concept of rank. This allows to deal only with sets of points and to capture relations between objects of the projective space (equality, collinearity, coplanarity, etc.) in a homogenous way. Taking advantage of the computational aspect of this approach, we automatically compute by saturation the ranks of all sets of the powerset of the points of the geometric configuration we consider. Upon completion of the saturation phase, our prover then retraces the proof process and generates the corresponding Coq code. This code is then formally checked by the Coq proof assistant, thus ensuring that the proof is actually correct. We use the prover to verify some well-known, non-trivial theorems in projective space geometry, among them: Desargues’ theorem and Dandelin–Gallucci’s theorem.

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.

Mechanizing proofs of geometric theorems in 3D is significantly more challenging than in 2D. As a first noteworthy case study, we consider an iconic theorem of 3D geometry: Dandelin-Gallucci's theorem. We work in the very simple but powerful framework of projective incidence geometry, where only incidence relationships are considered. We study and compare two new and very different approaches to prove this theorem. First, we propose a new proof based on the well-known Wu's method. Second, we use an original method based on matroid theory to generate a proof script which is then checked by the Coq proof assistant. For each method, we point out which parts of the proof we manage to carry out automatically and which parts are more difficult to automate and require human interaction. We hope these first developments will lead to formally proving more 3D theorems automatically and that it will be used to formally verify some key properties of computational geometry algorithms in 3D.

In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5th postulate. Our study is performed in the context of Tarski's neutral geometry, or equivalently in Hilbert's geometry defined by the first three groups of axioms, and uses an intuitionistic logic, assuming excluded-middle only for point equality. Our formalization provides a clarification of the conditions under which different versions of the postulates are equivalent. Following Beeson, we study which versions of the postulate are equivalent, constructively or not. We distinguish four groups of parallel postulates. In each group, the proof of their equivalence is mechanized using intuitionistic logic without continuity assumptions. For the equivalence between the groups additional assumptions are required. The equivalence between the 34 postulates is formalized in Archimedean planar neutral geometry. We also formalize a variant of a theorem due to Szmielew. This variant states that, assuming Aristotle's axiom, any statement which hold in the Euclidean plane and does not hold in the Hyperbolic plane is equivalent to Euclid's 5th postulate. To obtain all these results, we have developed a large library in planar neutral geometry, including the formalization of the concept of sum of angles and the proof of the Saccheri–Legendre theorem, which states that assuming Archimedes' axiom, the sum of the angles in a triangle is at most two right angles.

The geometric constructions obtained with only straightedge and compass are famous and play a special role in the development of geometry. On the one hand, the constructibility of figures is a key ingredient in Euclid geometry and, on the other hand, unconstructibility gave birth to famous open problems of the ancient Greece which were unlocked only in the nineteenth century using discoveries in algebra. This paper discusses the mechanization of straightedge and compass constructions. It focuses on the algebraic approaches and presents two methods which are implemented; one is due to Lebesgue and the other one was jointly designed by Gao and Chou. Some links between the algebraic approach of constructions and synthetic geometry are described.

Incidence geometry is a well-established theory which captures the very basic properties of all geometries in terms of points belonging to lines, planes, etc. Moreover, projective incidence geometry leads to a simple framework where many properties can be studied. In this article, we consider two very different but complementary mathematical approaches formalizing this theory within the Coq proof assistant. The first one consists of the usual and synthetic geometric axiom system often encountered in the literature. The second one is more original and relies on combinatorial aspects through the notion of rank which is based on the matroid structure of incidence geometry. This paper mainly contributes to the field by proving the equivalence between these two approaches in both 2D and 3D. This result allows us to study the further automation of many proofs of projective geometry theorems. We give an overview of techniques that will be heavily used in the equivalence proof and are generic enough to be reused later in yet-to-be-written proofs. Finally, we discuss the possibilities of future automation that can be envisaged using the rank notion.

We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues’ property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs.

In most cases in geometry, applying analytic or algebraic tools on coordinates helps to solve some difficult problems. For instance, proving that a geometrical construction problem is solvable using ruler and compass is often impossible within a synthetic geometry framework. But in an analytic geometry framework, it is a direct application of Galois theory after performing triangularizations. However, these algebraic tools lead to a large amount of computation. Their implementation in modern Computer Algebra Systems (CAS) are still too time consuming to provide an answer in a reasonable time. In addition, they require a lot of memory space which can grow exponentially with the size of the problem. Fortunately, some geometrical properties can be used to setup the algebraic systems so that they can be more efficiently computed. These properties turn polynomials into new ones so as to reduce both the degrees and the number of monomials. The present paper promotes this approach by considering two corpora of geometric construction problems, namely Wernick's and Connely's lists. These lists contain about 280 problems. The purpose is to determine their status i.e. whether they are constructible or not with ruler and compass. Some of these problems had unknown status that will be settled in this paper. More generally, the status of all problems of these corpora are fully automatically given by an approach combining geometry and algebra.

The goal of Point Distance Solving Problems is to find 2D or 3D placements of points knowing distances between some pairs of points. The common guideline is to solve them by a numerical iterative method (e.g. Newton–Raphson method). A sole solution is obtained whereas many exist. However the number of solutions can be exponential and methods should provide solutions close to a sketch drawn by the user. Geometric reasoning can help to simplify the underlying system of equations by changing a few equations and triangularizing it. This triangularization is a geometric construction of solutions, called construction plan. We aim at finding several solutions close to the sketch on a one-dimensional path defined by a global parameter-homotopy using a construction plan. Some numerical instabilities may be encountered due to specific geometric configurations. We address this problem by changing on-the-fly the construction plan. Numerical results show that this hybrid method is efficient and robust.

In many areas, some geometry problems can not be solved using only geometry and are treated by the means of algebraic tools. However, geometric properties can be still employed to simplify the system of equations. This allows either to speed up the treatment or, more radically, to make the treatment possible. In this article we illustrate this approach with a family of toy examples. In all these problems the goal it is to determine if there is a compass-and-straightedge construction of the three vertices of a triangle knowing only three located points of this triangle. Algebraic tools, basically Galois theory, are needed to answer the question. But in many cases a geometric reasoning phase is required to provide a polynomial algebraic system that algebraic softwares can address within a acceptable time despite the exponential complexity of the underlying algorithms.

Straightedge-and-compass construction problems are well known for different reasons. One of them is the difficulty to prove that a problem is not constructible: it took about two millennia to prove that it is not possible in general to cut an angle into three equal parts by using only straightedge and compass. Today, such proofs rely on algebraic tools difficult to apprehend by high school student. On the other hand, the technique of problem reduction is often used in theory of computation to prove other kinds of impossibility. In this paper, we adapt the notion of reduction to geometric constructions in order to have geometric proofs for unconstructibility based on a set of problems known to be unconstructible. Geometric reductions can also be used with constructible problems: in this case, besides having constructibility, the reduction also yields a construction. To make the things concrete, we focus this study to a corpus of triangle location problems proposed by William Wernick in the eighties.

We present a final status of all problems from Wernick’s list of triangle construction problems published in 1982 and with a number of unknown status until recently. Our results were obtained by a computer-based system for checking constructibility. We also developed a system for finding elegant constructions for solvable problems and for verifying their correctness. These systems helped in resolving problems open for decades, showing the power of modern computer systems in areas such as symbolic computation, problem solving, and theorem proving.

Straightedge and compass constructions play a special role in geometry. First, for a very long time, they were used in practice by land surveyors or architects in order to solve concrete problems. Second, they are an inexhaustible source of exercises used to learn concepts in geometry. And finally, some famous impossible problems related to straightedge and compass constructions waited centuries before being solved using algebra. In addition, not knowing if a well-constrained problem is constructible with straightedge and compass or not, make that kind of problems more difficult to address: should we synthesize a program or on the contrary find a counterexample has to be found and treated using algebra or reduction on it? In this paper, we perform a systematic checking of a whole corpus of problems proposed by William Wernick. We expose our methodology and the algorithm we used. For each problem, its constructibility status is computed and either an algebraic argument or a geometric construction is given.

This paper describes the formalization and implementation of a reflexive tactic for automated generation of proofs of incidence to an affine variety. Incidence proofs occur frequently in formal proofs of geometric statements. Nevertheless they are most of the time omitted in pen-and-paper proofs since they do not contribute to the understanding of the proof in which they appear. Our tactic allows us to automate proofs about incidence to an affine variety. Being based on a type class capturing the minimal set of properties needed to deal with incidence, the tactic is applicable to any theory verifying these properties. This type class is defined using dependent types to formalize predicates of parameterizable arity which represent the incidence to an affine variety.

Over the last sixty years, a number of methods for automated theorem proving in geometry, especially Euclidean geometry, have been developed. Almost all of them focus on universally quantified theorems. On the other hand, there are only few studies about logical approaches to geometric constructions. Consequently, automated proving of ∀∃ theorems, that correspond to geometric construction problems, have seldom been studied. In this paper, we present a formal logical framework describing the traditional four phases process of geometric construction solving. It leads to automated production of constructions with corresponding human readable correctness proofs. To our knowledge, this is the first study in that direction. In this paper we also discuss algebraic approaches for solving ruler-and-compass construction problems. There are famous problems showing that it is often difficult to prove non-existence of constructible solutions for some tasks. We show how to put into practice well-known algebra-based methods and, in particular, field theory, to prove RC-constructibility in the case of problems from Wernick’s list.

In this paper we focus on the formalization of the proof of equivalence between different versions of Euclid's 5 th postulate. This postulate is of historical importance because for centuries many mathematicians believed that this statement was rather a theorem which could be derived from the first four of Euclid's postulates and history is rich of incorrect proofs of Euclid's 5 th postulate. These proofs are incorrect because they assume more or less implicitly a statement which is equivalent to Euclid's 5 th postulate and whose validity is taken for granted. Even though these proofs are incorrect the attempt was not pointless because the flawed proof can be turned into a proof that the unjustified statement implies the parallel postulate. In this paper we provide formal proofs verified using the Coq proof assistant that 10 different statements are equivalent to Euclid's 5 th postulate. We work in the context of Tarski's neutral geometry without continuity nor Archimedes' axiom. The formalization provide a clarification of the hypotheses used for the proofs. Following Beeson, we study the impact of the choice of a particular version of the parallel postulate on the decidability issues.

The goal of Geometric Constraint Solving is to find 2D or 3D placements of some geometric primitives fulfilling some geometric constraints. The common guideline is to solve them by a numerical iterative method (e.g. Newton-Raphson method). A sole solution is obtained whereas many exist. But the number of solutions can be exponential and methods should provide solutions close to a sketch drawn by the user. Assuming that a decomposition-recombination planner is used, we consider irreducible problems. Geometric reasoning can help to simplify the underlying system of equations by changing a few equations and triangularizing it. This triangularization is a geometric construction of solutions, called construction plan. We aim at finding several solutions close to the sketch on a one-dimensional path defined by a global parameter-homotopy using the construction plan. Some numerical instabilities may be encountered due to specific geometric configurations. We address this problem by changing on-the-fly the construction plan. Numerical results show that this hybrid method is efficient and robust.

This paper describes some techniques to help building formal proofs in geometry and at the same time improving readability. Rather than trying to completely automate the proving process we provide symbolic manipulations which are useful to automate the parts of the formal proof that are usually implicit in a pen and paper proof. We test our framework using some well known theorems about triangles which are taught in high-school. We also highlight the proof steps which are usually overlooked in the informal proof and that we believe should be made explicit. Our framework is based on Tarski's geometry within the Coq proof assistant, but most of the ideas presented in this paper could be applied to other axiomatic systems or proof assistants.

In CAD, a designer usually specifies mechanisms or objects by the means of sketches supporting dimension requirements like distances between points, angles between lines, and so on. This kind of geometric constraint satisfaction problems presents two aspects which solvers have to deal with: first, the sketches can contain hundreds of constraints, and, second, the problems are invariant by rigid body motions. Concerning the first issue, several decomposition methods have been designed taking invariance into account by fixing/relaxing coordinate systems. On the other hand, some researchers have proposed to use distance geometry in order to exploit invariance by rigid body motions. This paper describes a method that allows us to use distance geometry and decomposition in the same framework.