Seminaire ITI IRMIA : Julien Narboux : Mechanical verification of proofs in geometry

The next seminar of our Interdisciplinary Thematic Institute (ITI) IRMIA++ will be held this Thursday October 20th at 09:00 am, both in the IRMA conference room and on BBB.

The talk will be given by: Julien NARBOUX (ICube).

Title:  Mechanical verification of proofs in geometry

BBB link: https://bbb.unistra.fr/b/hum-51d-suf-mzq

Abstract:  The first part will consist of a short introduction to the field of computer verified proofs. Why verify proofs with a computer? what can be verified? what are the challenges? In a second part, I will give an overview of our formalizations concerning the foundations of geometry based on the axiom systems of Hilbert, Tarski and Euclid. In particular, I will present a joint work with Michael Beeson and Freek Wiedijk which consisted in mechanically verifying the proofs of the first book of Euclid's Elements while trying to stay as close as possible to the original proofs. I will discuss the classification of 34 versions of the axioms of parallels (joint work with Pierre Boutry). We will finish by presenting a syntactic proof of the independence of the axiom of parallels (joint work with Michael Beeson and Pierre Boutry).

His research interests include formal proofs and formalisation of foundations of geometry and applications.
He is especially interested in automated reasoning (in particular in geometry) and using proof assistants for teaching.