Mathematics 161
Introduction to formal verification of mathematics (220544)
Philip Wood2026 Spring (4 Credits)
Schedule: MW 1:30 PM - 02:45 PM
Instructor Permissions: None
Enrollment Cap: n/a
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.
: