Inria, Sophia Antipolis
My principal interests of research are in formalization and foundations of geometry.
Inria, Sophia Antipolis
University of Strasbourg, ICube Laboratory
University of Strasbourg, ICube Laboratory
Chalmers University of Technology, Gothenburg
I am interested in the foundations of geometry and their formalization within the Coq system using the Mathematical Components library. I obtained a Ph.D. on ways to axiomatize Euclidean geometry, statements of the parallel postulate and the possibilities of automating geometric reasoning. I have notably contributed to the discovery of a new proof of the independence of the parallel postulate.
We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line ℂP1 and is shown to satisfy Tarski's axioms except for Euclid's axiom — it is shown to satisfy it's negation, and, moreover, to satisfy the existence of limiting parallels axiom.
Dans cet article, nous présentons les résultats sur la continuité que nous avons obtenus dans le cadre du projet GeoCoq, qui constitue une formalisation en Coq de la géométrie : nous avons défini 11 axiomes de continuité et établi leur hiérarchie. Nos démonstrations ont été formalisées dans le cadre de la géométrie neutre de Tarski en dimension quelconque et de la logique intuitionniste.
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 leads us to refine Pejas' classification of parallel postulates. We do so by considering decidability properties when classifying the postulates. However, our intuition often guides us to overlook uses of such properties. A proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants let us leverage the computational capabilities of computers. We demonstrate how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we present a specific procedure designed to automate proofs of incidence properties.
In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th 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 theorem due to Szmiliew. This theorem states that, assuming Archimedes' axiom, any statement which hold in the Euclidean plane and does not hold in the Hyperbolic plane is equivalent to Euclid's 5 th 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.
This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamath-ematical properties. This work completes our formalization of the two-dimensional results contained in part one of the book by Schwabhäuser Szmielew and Tarski Metamathematische Methoden in der Geometrie. We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a " back-translation " from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski's Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the Gröbner basis method. Moreover , we solve a challenge proposed by Beeson: we prove that, given two points, an equilateral triangle based on these two points can be constructed in Euclidean Hilbert planes. Finally, we derive the axioms for another automated deduction method: the area method.
This paper describes the formalization of the arithmetization of Euclidean geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamathematical properties. This work completes our formalization of the two-dimensional results contained in part one of [SST83]. We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a " back-translation " from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski's Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the Gröbner basis method.
Nous nous intéressons dans cet article au 5e postulat d'Euclide. Ce postulat a une importance historique : pendant des siècles, de nombreux mathématiciens de renom ont cru que cet axiome était un théorème qui pouvait être dérivé des quatre premiers postulats d'Euclide. Dans cet article nous présentons la formalisation en Coq de résultats concernant le lien entre l'unicité de la parallèle et le fait que la somme des angles d'un triangle est égale à deux droits. Nous travaillons en logique intuitionniste dans le contexte de l'axiomatique de Tarski. D'une part nous obtenons la preuve formelle de l'équivalence et d'autre part nous clarifions les propriétés de décidabilité nécessaires pour la preuve. Nous étudions également le lien entre l'axiome d'Aristote et la décidabilité de l'intersection entre deux droites.
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.
We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.
In this paper we study some decidability properties in the context of Tarski's axiom system for geometry. We removed excluded middle from our assumptions and studied how our formal proofs of the first thirteen chapters of [SST83] were impacted. We show that decidability of equality is equivalent to the decidability of the two other given predicates of the theory: congruence and betweenness. We prove that the decidability of the other predicates used in [SST83] can be derived except for the predicate stating the existence of the intersection of two lines. All results have been proved formally using the Coq proof assistant.
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 informal proofs 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.
The goal of the course is to present inductively defined sets, proofs by induction, propositional and first-order logic and resolution. In addition, the soundness and completeness of the rules of both propositional and first-order logic is demonstrated.
The course covers the principles and pratice of programming in a functional language, illustrated with the use of the OCaml language. Its aim is to introduces the functional kernel of the OCaml language, exception handling, sum types, inductive types, recursion, higher-order functions and modules while emphasising the notion of persistent data structure. These concepts are practiced through the study of different implementations of sets as lists, binary search trees or AVL trees as well as maps and suffix trees.
The aim of the course is to give to students with a background in computer science the opportunity to obtain a reliable basis in mathematics. The different lessons focus on the most crucial mathematical concepts for a future engineer: functions of a real variable, complex numbers, polynomials, matrices, matrix diagonalization, integral calculus, Taylor series, integrability, numeric sequences and series, power series.
The course serves as an introduction to the tools for formal proofs and certification of softwares through the use of the Coq proof assistant. It covers the definition of types, functions, propositions of proofs, the relationship between mathematics and programming, definitions and proofs by induction as well as notions of certification and program extraction from proofs.
The course consists of two parts. During the first part, basic linear algebra concepts like matrix algebra, vector and matrix norms, error analysis or condition numbers, several variants of Gaussian elimination, some stationary iterative methods and analysis of algorithms are studied. The second part focuses on numerical methods for ordinary differential equations and their analysis.
This is an introductory course in programming, using the imperative language C as the medium of instruction. It describes the concepts of variables, iterative and recursive algorithms, iterations, functions, IO and streams, file management, standard and external librairies, memory allocation, pointer and pointer arithmetic. Moreover, it gives an overview of sorting algorithms and data structures such as vectors, string, lists, trees or binary search trees.
The course is divided into two parts. The first part provides an introduction to linear programming, branch-and-bound algorithms, dynamic programming and algorithms for shortest path problems, scheduling and flow problems. The second part covers stochastic processes, queueing theory and inventory theory.
I would be happy to talk to you if you need my assistance in your research or whether you are a student with a question regarding the courses in which I teach. You can find at either of the following places. Although, most of the time I will be at my lab.
You can no longer find me at the places listed below, but, due to the current global pandemic, a physical meeting is unlikely so I did not bother updating this information.