Events

13 June 2008

Jeremy Avigad,
Carnegie Mellon University,
June 13, 2008, 11h,
MSR-INRIA Joint Centre,
bat I, Parc Université Club, Orsay

A formal system for Euclid’s *Elements*
(joint work with Ed Dean and John Mumma)

For more than two thousand years, Euclid’s *Elements* was viewed as the paradigm of rigorous argumentation. But this changed in the nineteenth century, with concerns over the use of diagrammatic inferences and their ability to secure general validity. Axiomatizations by Pasch, Hilbert, and later Tarski are now taken to rectify these shortcomings, but proofs in these axiomatic systems look very different from Euclid’s.

In this talk, I will argue that proofs in the *Elements*, taken at face value, can be understood in formal terms. I will describe a formal system with both diagram- and text-based inferences that provides a much more faithful representation of Euclidean reasoning, and is sound and complete for the class of theorems that can be expressed in the language. Both types of inferences are smoothly verified by SMT back ends. This makes it possible to formally verify Euclidean diagrammatic proofs, and provides useful insight into the nature of mathematical proof more generally.