Proof-checking Euclid

TL;DR

This paper employs computer proof-checking methods to verify and extend Euclid's Book I propositions, filling gaps, correcting errors, and ensuring rigorous correctness using formal logic and proof assistants.

Contribution

It introduces a formal verification of Euclid's propositions using modern proof checkers, filling gaps and correcting errors in Euclid's original proofs.

Findings

Verified 235 propositions in Euclid Book I

Filled gaps and corrected errors in Euclid's proofs

Demonstrated the effectiveness of formal proof checkers for classical geometry

Abstract

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 235 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.