Redirecting to new page

Academic Positions

  • Present 2019

    Postdoctoral researcher

    Inria, Sophia Antipolis

  • 2018 2013

    Ph.D. student

    University of Strasbourg, ICube Laboratory

  • 2017 2016

    ATER[W]

    ENSIIE, Strasbourg

  • 2016 2013

    Teaching assistant

    ENSIIE, Strasbourg

Education & Training

  • 2018 2013

    Ph.D. student

    University of Strasbourg, ICube Laboratory

  • 2013 2011

    M.Sc., Engineering Mathematics and Computational Science

    Chalmers University of Technology, Gothenburg

  • 2011 2009

    Engineering Degree, M.Sc. equivalent

    ENSIIE, Strasbourg

Main Co-Authors

Gabriel Braun

Associate professor

His Web page

Pascal Schreck

Professor

His Web page

Julien Narboux

Associate professor

His Web page

Gabriel Braun

Associate professor

His Web page

Pascal Schreck

Professor

His Web page

Julien Narboux

Associate professor

His Web page

Filter by type:

Sort by year:

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Danijela Simić, Filip Marić, Pierre Boutry
Journal Paper Journal of Automated Reasoning, Springer Verlag, 2020

Abstract

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.

Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq

Charly Gries, Julien Narboux, Pierre Boutry
Conference Paper Les trentèmes Journées Francophones des Langages Applicatifs (JFLA 2019), Jan 2019, Les Rousses, France. 2019, Actes des Trentièmes Journées Francophones des Langages Applicatifs (JFLA 2019).

Abstract

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.

On the Formalization of Foundations of Geometry

Pierre Boutry
ThesisPh.D. thesis, Université de Strasbourg, 2018.

Abstract

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.

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck
Journal Paper Journal of Automated Reasoning, Springer Verlag, 2017

Abstract

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.

Formalization of the Arithmetization of Euclidean Plane Geometry and Applications

Pierre Boutry, Gabriel Braun, Julien Narboux
Journal Paper Journal of Symbolic Computation, Elsevier, 2017, Special Issue on Symbolic Computation in Software Science

Abstract

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.

From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry

Pierre Boutry, Gabriel Braun, Julien Narboux
Conference Paper SCSS 2016 The 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan.

Abstract

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.

Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq

Charly Gries, Pierre Boutry, Julien Narboux
Conference Paper Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint Malo, France. 2016, Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016).

Abstract

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.

A reflexive tactic for automated generation of proofs of incidence to an affine variety

Pierre Boutry, Julien Narboux, Pascal Schreck
Unpublished Paper

Abstract

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.

Herbrand's theorem and non-Euclidean geometry

Michael Beeson, Pierre Boutry, Julien Narboux
Journal Paper Bulletin of Symbolic Logic, Association for Symbolic Logic, 2015, 21 (2), pp.12

Abstract

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.

A short note about case distinctions in Tarski's geometry

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
Conference Paper Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp. 51–65, 2014, Proceedings of ADG 2014.

Abstract

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.

Using small scale automation to improve both accessibility and readability of formal proofs in geometry

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
Conference Paper Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp. 31–49, 2014, Proceedings of ADG 2014.

Abstract

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.

Teaching History

  • 2017 2014

    Mathematical logic

    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.

  • 2017 2016

    Functional programming

    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.

  • 2017 2016

    Mathematical tools

    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.

  • 2017 2016

    Proof engineering

    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.

  • 2016 2013

    Numerical analysis

    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.

  • 2016 2015

    Imperative programming

    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.

  • 2014 2013

    Operations research

    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.