Specifications, Constraints and Proofs in Geometry Assessment2016-2021

Objectives / Challenges

The objectives of this theme are the formalization of geometry for practical uses such as the resolution of geometric constraints, the aid to proof in geometry in the fields of education or robotics or the certification of algorithms related to geometry. This is a difficult topic where theoretical aspects such as formal algebraic calculus, the theory of the calculus of constructions or the axiomatization of geometry coexist with more practical aspects such as the engineering of the proof in Coq or the guidance of numerical methods developed in C++.

Participants

Results

Mechanization of constructions with ruler and compass

This problematic has been, in the team, essentially studied by P. Schreck and P. Mathis. Some results have been obtained and published with Predrag Janicic and Vesna Marinkovic from the University of Belgrade (Serbia).

The most important result is the algebraic proof in Maple of the constructibility status of two lists of construction problems known to American mathematicians as Wernick's list and Connelly's list. These lists contain about 270 problems of construction with ruler and compass from characteristic points, they were created in a systematic way as an amusement and a challenge for mathematics teachers, mainly in high school, and have received partial answers from various mathematicians in the world. The originality of our work is mainly to have developed a method to automatically process the two lists and to deliver the status, roughly constructible or non-constructible with ruler and compass, of each problem. On this occasion, we implemented what makes our approach unique: we mixed formal geometric reasoning, implemented as a Prolog program, to guide the shaping and triangularization of algebraic systems in the form of regular strings, the latter being processed by Maple to obtain the corresponding Galois groups, all of which was implemented by a Maple program [2-SM19].

It should be noted that the aim here is to test the constructability and not to exhibit, eventually, a construction. The last results of our team in this domain are a comparison of a method due to Lebesgue, and which we have improved, and a method due to Chou and Gao [2-Schr19]. A challenge is to take advantage of this study to have a feasible method for equations of degree 8.

Foundations of geometry

Taking over a work of J. Narboux and then G. Braun, P. Boutry devoted a large part of his thesis to the formalization in Coq of Tarski's book on the foundations of geometry. One of the tricks of P. Boutry's thesis was a very meticulous study of more than twenty propositions equivalent under certain conditions to the axiom of parallels. By closely examining these equivalence conditions, P. Boutry established a dependency graph (from the strongest to the weakest) of these axioms. The use of Coq was essential here, because there were many opportunities to make mistakes by assuming a so-called obviousness [2-BGNS17].

Help to the proof in incidence geometry

This point covers mainly the thesis work of David Braun, PhD student co-supervised by N. Magaud and P. Schreck. The very ambitious objective of this thesis was to identify ways of helping to make proofs with geometry as an experimental field. It is indeed not easy to make proofs in geometry, in particular because of the double nature of the "figure" which is often used as a support for the proof: on the one hand, this figure is necessary, at least for some mathematicians, to have the intuition of the proof by making it possible to identify known patterns, and on the other hand, this figure is a particular, often false, instance of the specification, and can therefore easily mislead and lead to "proofs" which lead nowhere. Because it is a domain we know well, we have chosen to study projective geometry from this point of view because it is easy to axiomatize, it hides a formidable complexity and the absence of notions like distances or angles requires a great rigor in the reasoning. The main results obtained were diverse and can be grouped into the following points (detailed below):

• equivalence between the synthetic approach and a very general combinatorial structure, the matroids,
• study of a proof technique to take into account large combinatorial proofs in the framework of finite geometries,
• design and implementation of an automatic matroid-based prover.

1. Equivalence between the synthetic approach and the combinatorial approach via matroids.

This work completes a study already done by the team [2-MNS12] where a sense of equivalence had been established. The other sense of equivalence (from matroids to geometry) required a consequent development where the "object oriented" techniques of Coq were implemented to decouple well the different notions and to differentiate, in particular, the dimensions 2, 3 and beyond three, i.e. without axioms indicating an upper bound for the dimension. This work has been published in a referenced journal of the field [2-BMS19], and it has been used to justify further work using intensively this matroid approach.

2. Finite incidence geometries

This study of some projective incidence structures has been the occasion of stress test for Coq and for the programmer in Coq. Indeed, these structures imply a combinatorial explosion to the point that there are many open questions on this subject, such as, for example, the existence of an incidence plane of order 12, i.e. with 13 points per line if we consider the projective case. This was the occasion to develop strategies to make Coq handle the proofs without memory overflow and in a reasonable time. It is also during this study that a comparison between the synthetic approach and the matroid-based approach in terms of complexity was carried out. Depending on the case, one approach is better than the other and vice versa [4-BMS18]. However, one of the great advantages of the matroid-based approach is that it can be automated and that it treats the problems homogeneously with respect to the dimension of the projective space.

3. An automatic matroid-based prover

This prover is very specialized and consists in filling a matroid structure represented by a rank function from the data of the statement. It thus requires to have eliminated all existential quantifiers. Although it seems limited, it has allowed to prove formally and with a great degree of automation, various key theorems of incidence geometry in dimension 2 and 3 and in particular, the Dandelin-Gallucci theorem [8-Brau19].