Universiteit van Amsterdam


Institute for Logic, Language and Computation

25 October 2017, Proof-checking Euclid, Michael Beeson

Speaker: Michael Beeson
Date: Wednesday 25 October 2017
Time: 12:00-14:00
Location: Ravensteynzaal, Kromme Nieuwegracht 80, 3512 HM Utrecht

This is 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. Then we checked those proofs in the well-known and trusted proof checkers HOL Light and Coq. The talk will contain many geometrical diagrams and discuss both the geometry and the proof-checking.