LSV Seminar

Date

04.01.2021, 16:00

Place

online

Speaker

Pierre Boutry (Inria Sophia Antipolis)

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 talk, 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. We also 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. It requires that “we take the extreme measure of shutting out the entreaties of our intuitions and imaginations”. To help us in this task, a proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Then, we present our progress towards obtaining an independent version of Tarski's axioms. Finally, we report on the advance of the project of proving the isomorphism between two models of hyperbolic geometry formalized in two different proof assistants.