Seminar Details

We will give an introduction to the formalization of Euclid’s elements in the Lean Theorem Prover, which is a software tool for formally writing and verifying mathematical proofs. Seminar participants should leave with the technical knowledge in order to start formalizing proofs of the Pythagorean theorem as part of the research theme of the Spring 2023 seminar. This research theme ultimately has implications for studying the topology of the space of proofs of the theorem and for data augmentation used for neural theorem proving, the application of machine learning and Lean to automatically produce mathematical proofs. Participants should have Lean 3 installed on their computer before the seminar (for installation, please visit https://leanprover-community.github.io/get_started.html or reach out to an organizer (Brittany Gelb, <bg545 at math.rutgers.edu>) for assistance.)