University of Strasbourg, ICube Laboratory
Prior to beginning the Ph.D. program, I studied Mathematics at Chalmers University of Technology and Computer Science at ENSIIE.
My principal interests of research are in formalization and foundations of geometry.
University of Strasbourg, ICube Laboratory
University of Strasbourg, ICube Laboratory
Chalmers University of Technology, Gothenburg
Technological tools are widely used to teach mathematics in schools. Dynamic Geometry Software (D.G.S.) and Computer Algebra Software (C.A.S.) are the two software families that are well represented. On the one hand, these tools are extensively used to explore, experiment, visualize, calculate, measure, find counter example and conjecture. Basically, they make mathematics more experimental. They, however, fail as tools assisting students in making a formal proof. We have the conviction that the reasoning and the concept of a proof should both have a crucial place in mathematics teachings. This calls for a computer-based learning environment for interactive proofs. On the other hand, proof systems such as Coq and Isabelle are far too general and complex for direct use in science and mathematics education. Thus our objective is to develop tools and libraries for formal proof in geometry adapted to educational contexts.
As a basis for these tools and libraries, Tarski's system of geometry was chosen for its well-known metamathematical properties. We started by formally proving a few theorems with Coq that are usually given to high school students in order to understand the differences between pen-and-paper proofs and formal proofs. We isolated a few problems which are encountered while establishing a formal proof. We then developed some techniques to help build formal proofs in synthetic geometry, this simultaneously improved readability. The first technique automatically applies low-level lemmas and hides them to deal with permutation properties of some geometric predicates. A second technique helps to prove non-degeneracy-conditions (NDCs) when dealing with degenerate cases. A third technique uses reflexive functions to deal with combinatorial explosions when dealing with basic incidence axioms. We observed that the idea behind the latter could be generalised. Therefore we introduced the modifications necessary to obtain a significantly more powerful tool which would be of great help when we will extend our already proven lemmas to dimensions higher than 2. Recently we have started rethinking the way of handling permutation properties of some geometric predicates and we consider implementing a reflexive tactic which would deal with this issue.
While studying the differences between pen-and-paper and formal proofs, it was observed that case distinctions were made very often. This motivated our research in studying some decidability properties in the context of this system by removing excluded middle from our assumptions. Having done so, we proved that decidability of equality of points is equivalent to the decidability of the two other given predicates given in the theory: congruence and betweenness. It was also proved that the decidability of the other predicates used in the book Metamathematische Methoden in der Geometrie by Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski can be derived except for the predicate stating the existence of the intersection of two lines. Furthermore, working in collaboration with Michael Beeson, Herbrand’s theorem was used to give a new proof that Euclid’s parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. The main contribution of this paper is that we proved the independence without actually constructing a model of non-Euclidean geometry. In one of his recent papers, Michael Beeson suggested the possibility of obtaining a fully constructive formal development about Tarski’s geometry. Our work is a first step towards achieving this goal, which we consider relevant in the context of mathematics education for the following reason. One of the axiomatic systems he proposed corresponds to ruler-and-compass type construction. A proof of the existence of a point in this system, is a construction of this point using a ruler and a compass. Using this system would thus allow us to provide students with ruler-and-compass construction problem.
During this team work, one of Beeson's recent papers gave us the idea of replacing an axiom (Tarski's version of the parallel postulate) by a classically equivalent one, which allowed us to remove the decidability of the existence of the intersection of two lines from our assumptions (later, we proved that Tarski's version of the parallel postulate also implies the decidability of the existence of the intersection of two lines). This encouraged us to start working on proving equivalences of several versions of this axiom. We are currently writing a paper about the formalization of the equivalence proofs, in which we provide formal proofs, verified using Coq, that 29 different statements are equivalent to Euclid’s 5th postulate. We worked in the context of Tarski’s neutral geometry without continuity nor Archimedes' axiom. The formalization provides clarification of the hypotheses used for the proofs. Following Beeson, we studied the impact of the choice of a particular version of the parallel postulate on the decidability issues. Moreover, we studied which versions of the parallel postulate require Archimedes' axiom to be proven equivalent to Playfair's postulate.
Finally we are currently working with Cyril Cohen on proving that real closed fields are models of Tarski's geometry and that Tarski's geometry is a model of real closed fields. This will allow us to show the relative consistency and the satisfiability of Tarski's system of geometry. Moreover, we are also working on proving that the quantifier elimination procedure programmed by Cyril Cohen and Assia Mahboubi can be applied to Tarski's system of geometry and decidability (first established by Tarski) of the full first order theory of any instance of Tarski's system of geometry with decidable equality. Being able to verify that the axiomatic system, selected in this work presents many important metamathematical properties would allow us to reach a higher level of confidence in the proofs based on it which is crucial in our context.
We recently proved[Link] that in any model of planar Tarski's geometry one can construct a cartesian plane over pythagorean ordered fields in which the Gröbner basis method can be applied. One of the problems tackled while developing our techniques, was the NDCs of lemmas. It will be interesting to investigate the use of Wu's method, which can also be applied in this cartesian space, to provide minimal NDCs for a given lemma. Wu's method would then be considered as a possible way of automatically proving ad-hoc axioms (from the axioms of Tarski's geometry), that students assume when studying geometry during high school. This would allow the students to do formal proofs based on these ad-hoc axioms (where some of the techniques we developed could be used to make the proving process more feasable for a high school student) but at the same time allow a high level of confidence since the proof would rely on Coq (a well-trusted proof assistant) and Tarski's geometry (a well-studied axiomatic system).
Our studies suggest several lines of research for future work. For example, using Coq we would also like to verify the suggestion made by Michael Beeson in or to instantiate other automated deduction methods or axiomatic systems such as Wu's method or real closed fields.
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.
In this paper we focus on the formalization of the proof of equivalence between different versions of Euclid's 5 th postulate. This postulate is of historical importance because for centuries many mathematicians believed that this statement was rather a theorem which could be derived from the first four of Euclid's postulates and history is rich of incorrect proofs of Euclid's 5 th postulate. These proofs are incorrect because they assume more or less implicitly a statement which is equivalent to Euclid's 5 th postulate and whose validity is taken for granted. Even though these proofs are incorrect the attempt was not pointless because the flawed proof can be turned into a proof that the unjustified statement implies the parallel postulate. In this paper we provide formal proofs verified using the Coq proof assistant that 10 different statements are equivalent to Euclid's 5 th postulate. We work in the context of Tarski's neutral geometry without continuity nor Archimedes' axiom. The formalization provide a clarification of the hypotheses used for the proofs. Following Beeson, we study the impact of the choice of a particular version of the parallel postulate on the decidability issues.
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 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.
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 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.