Geometry is central in both the history and teaching of the structure of mathematical proofs and the axiomatic method.

In this talk, we will give an overview of the GeoCoq library. The library developed in collaboration with P.Boutry, G. Braun, C. Gries and P. Schreck consists in a formalization of geometry using the Coq proof assistant.

Starting from the foundations based on either Euclid’s, Tarski’s, or Hilbert’s axiom systems, we formalized the traditional results which can be used for high-school exercises.

We will discuss the axiomatizations and the automation necessary for use in the classroom.

Based on some examples taken from highschool exercices, we will revisit some traditional proofs from a formal point of view.