Thesis: On the Formalization of Foundations of Geometry

PhD defense: Pierre BOUTRY

Team: IGG

Title: On the Formalization of Foundations of Geometry

Abstract: Geometry has always had an important role in the evolution of the foundation of mathematics. For example, Euclid introduced the axiomatic method with his Elements. While Euclid's work was considered as a paradigm of rigorous argumentation for over 2000 years, Moritz Pasch pointed out the need for an additional axiom in 1882. Since Automath, the first logical framework designed in 1967, a plethora of proof assistants have been developed, allowing, amongst other things, to avoid such implicit assumptions. In this thesis, we investigate how a proof assistant can be used to study the foundations of geometry. We start by focusing on ways to axiomatize Euclidean geometry and their relationship to each other. Then, we expose a new proof that Euclid’s parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. This independence proof leads us to refine Pejas' classification of parallel postulates. We do so by not only considering continuity axioms, but also decidability properties to determine whether two versions of this postulate are equivalent or not. As Richard J. Trudeau has written, proving the equivalence of different versions of the parallel postulate without assuming decidability properties or continuity axions requires extreme rigor. To help us in this task, a proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants are valuable in the context of geometry in another way: they let us leverage the computational capabilities of computers. In fact, geometry is one of the fields in which automated theorem proving has been very successful. Thus, we present how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we demonstrate how a specific procedure designed to automate proofs of incidence properties allowed us to handle issues arising when assuming a theory such as Tarski's system of geometry.

The jury is comprised of:

• Mr. Thierry Coquand (Professor, University of Gothenburg)
• Mr. Gilles Dowek (Research director, Inria)
• Mr. Predrag Janičić (Professor, University of Belgrade)
• Mrs. Assia Mahboubi (Researcher, Inria)
• Mr. Julien Narboux (Associate professor, University of Strasbourg)
• Mr. Pascal Schreck (Professor, University of Strasbourg)

The defense will be held on Tuesday, November 13th, at 2:30 pm in the JF Lefevre amphitheater of the Pole API building in Illkirch (building I).