Recent searches
Search options
A #Lean4 formalisation of Book 1 of Euclid
André Hernández-Espiet, "Formalized synthetic geometry"
https://doi.org/doi:10.7282/t3-cb1v-a415
Abstract: We offer a formalization of Book I of Euclid’s Elements in Lean4 (with tools fromMathlib4) using System E by Avigad, Dean, and Mumma. We contrast the proofs in this system to those of Euclid’s himself. We give detailed explanations for every theorem proved in Lean4 in order to complete Book I. Finally, we talk about the importance of tactics in Lean4 for the shortening and simplification of the proofs encountered in a geometric setting.
h/t @Jose_A_Alonso
"System E" is a formal system for Euclidean geometry that is deliberately trying to hew closely to what Euclid actually did, but in a watertight way. So not eg Hilbert's axioms or Tarski's in place of Euclid's.
https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf
@highergeometer - nice, because it takes into account the role of diagrams, which are needed in Euclid's arguments, e.g. to indicate 'betweeness relations' between points on a line.
@highergeometer Today I Learned System E is a thing. I found it hard to read Euclid from the point of view of wanting the reasoning to be watertight. My previous reaction was to think Tarski's axioms are the best way out, and perhaps they still are, but something which more directly tries to make sense of Euclid as written is intriguing.
@highergeometer @Jose_A_Alonso
Interestingly, this thesis has 27 pages of main content, and ~200 pages of appendices.
Definitely a nontraditional organization! :-)