Meeting Time: Monday 12:00 PM - 01:15 PM; Wednesday 12:00 PM - 01:15 PM
Course Description: How can a computer check if a mathematical proof is completely and truly correct? This course will be an introduction into the world of formal verification of mathematics, starting with basic examples of sets and natural numbers, and moving on to more advanced mathematics. We will work with Lean, an open-source programming language for formal verification that has been used to verify large portions of mathematics, including a few examples reaching all the way to the forefront of current mathematics research.
The general plan is to work through parts of the book Mathematics in Lean by Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, and Patrick Massot to give everyone a foundation in implementing mathematics in Lean. A large portion of the course will be dedicated to working on individual projects implementing mathematics in Lean. The main course page will be on Canvas (you will need a Harvard account to gain access).
Try the Natural Numbers Game to get a sense what it means to implement mathematics proofs in Lean!
To find out more details about the course, have a look at the Syllabus, and if you have questions about the course, please send me an email.
Finally, I want to say thanks to Jeremy Avigad for sharing materials for a similar course taught at CMU in Fall 2022. I also want to thank Kevin Buzzard, Robert Lewis, and Patrick Massot for sharing course materials for related Lean courses, and also thanks to the organizers and everyone else at the 2022 conference on Lean at ICERM.
--Philip Matchett Wood