Formalization of Tarski's geometry in the Coq proof assistant.


Gabriel Braun and Julien Narboux and Pierre Boutry

In the early 60s, Wanda Szmielew and Alfred Tarski started the project of a treaty about the foundations of geometry. A systematic development of euclidean geometry based on Tarski's axioms was supposed to constitute the first part, but the early death of Wanda Szmielew  put an end to this project. Finally, Wolfram Schwabhäuser continued the project of Wanda Szmielew and Alfred Tarski. He published the treaty in 1983 in German : Metamathematische Methoden in der Geometrie.

We present here the formalization within the Coq proof assistant of the first 15 chapters of this book.
We also prove that Hilbert axioms can be derived from Tarski axioms (this proof does not include the continuity axioms).

Related papers:

Here is an illustrated presentation of the axioms, the main definitions and an example of a proof (in french).

Here is a .pdf file containing all the defintions and the lemmas (without proofs) .

Here is a .tgz containing all the Coq files (updated 04/2014).

You can browse the Coq files from the index or you can have a look at one of the following chapters :


W. Schwabhäuser
W Szmielew
A. Tarski

Metamathematische Methoden in der Geometrie

Mit 167 Abbildungen


Teil I:Ein exiomatischer Aufbau der euklidischen Geometrie
von W.Schwabhäuser, W. Szmielew und A. Tarski

Teil II:Metamathematische Betrachtungen
von W. Schwabhäuser


Springer-Verlag 1983
If you are interested in the dependency graph of the Coq theorems used for this proof, i generated the graph using a tool developed by Anne Pacalet called DpdGraph:
The graph in .svg format is so big that it is difficult to visualize within your browser, I advise you to use a tool such as ZGRViewer as in the applet below.
At the bottom you will find the logical connectives (and, ex, ...). On the right, you will find the definition of equivalence relation for the setoid equalities. The 12 chapters (depicted as yellow boxes) are used for the proof of Hilbert's axioms.

Dependencies viewer: