skip to: page content | links on this page | site navigation | footer (site information)

Michael Beeson's Research

Utility Link | Utility Link | Utility Link
-->

Proof Checking Euclid

Joint work with Julien Narboux and Freek Wiedijk

We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid's gaps and correcting errors. Euclid Book I has 48 propositions; we proved 213 theorems. The extras were partly ``Book Zero'', preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid's gaps, and partly just variants of Euclid's propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid's logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq.

This web page provides (below) links to all the files needed to reproduce this work. The paper that describes the work can be found here:

Proof-checking Euclid

Persons wishing to download the files necessary to reproduce our work may download them all at once in the following archive:

proofs.tar.gz

In that archive, you will find more than 200 proofs, in files ending in .prf, as well as some PHP scripts (ending in .php). The steps to reproduce our work are as follows:

(1) Ensure that PHP is installed on your system, then run 

 ./Checkproofs.php
from the directory in which you unpacked the archive. This runs our custom proof-checker, or proof debugger, on all the proofs. That one PHP file contains all the source code for our custom proof-checker.

(2) The script FreekFiles.php has already been run to produce the .ml files included in the archive. Ensure that HOL Light is running on your system. To check these proofs in HOL Light, see [link not yet live]

(3) The script CoqExport.php has already been run to produce the .v files. Those are included in GeoCoq library. To compile GeoCoq you need Coq version 8.5pl3 or 8.6.1 or 8.7beta see instructions given here.