19 March 2018: Imogen Morris

A Mechanization in Isabelle of Birkhoff's Ruler and Protractor Geometry, following Brossard

In a paper published in 1931, Birkhoff gave a set of axioms which were designed to encapsulate the ruler and protractor in Euclidean Geometry. Since these axioms are at a higher-level than those given, for example, by Hilbert or Tarski, they should provide a quicker route to formally deriving theorems in metric geometry. However, mechanizing these axioms and results in the proof-assistant Isabelle brings some challenges. Many of Birkhoff's statements require interpretation before they can be formalised, so we follow Brossard's paper, 'Birkhoff's Axioms for Space Geometry', which represents Birkhoff's axioms more formally. In this talk I will discuss the mechanization and I will attempt to decipher Birkhoff's mysterious hint of non-Archimedean possibilities for angles.