News and Events: Upcoming Events

Please note that this newsitem has been archived, and may contain outdated information or links.

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.

Please note that this newsitem has been archived, and may contain outdated information or links.