Formal Euclidean Geometry

Course Description: This course explores classical Euclidean geometry through a modern lens, using the Lean4 proof assistant to formalize definitions, theorems, and proofs. Students will gain deep understanding of geometric reasoning while learning contemporary approaches to mathematical formalization.

Lecture	Topic & Content	Lecture Notes
07/07/25	Lecture 1 Engineering vs Mathematics Truth + Proof Truth + Proof + Axioms Euclid's Elements The Parallel Postulate	📝 Lecture 1 Notes
07/08/25	Lecture 2 Proposition I.1 Platonic Solids Hyperbolic Geometry Parallel Postulate	📝 Lecture 2 Notes
07/09/25	Lecture 3 In Non-Euclidean Geometry, AAA Implies Congruence Gap in Euclid's Prop I.1 David Hilbert's Ideas on Formalization Undefined Terms Beginning Formalization	📝 Lecture 3 Notes

Course Resources

📚 Primary Text: Euclid's Elements (Joyce Edition)
📺 Codespaces: Lean's Math library codespace
📖 Mathlib: Mathlib4 Documentation