Course: 80-419/719, Spring 2019
Instructor: Jeremy Avigad (firstname.lastname@example.org)
Time: MW 1:30-2:50
Interactive theorem proving involves the use of computational proof assistants to verify that mathematical claims are correct, or to verify that hardware and software designs meet their formal specifications. In this course, we will explore this new technology and its logical foundations. Topics include:
The course will make use of a new interactive theorem prover called Lean and its mathlib library. Initially, we will follow an online text, Theorem Proving in Lean. We will likely make use of CoCalc, an environment for mathematical collaboration in the cloud.
The grade for the course will be based on assignments and projects. For the most part, these will involve formalization using Lean.
The course can be taken at the undergraduate or graduate level. Undergraduates are required to have a course in logic (80-211, 80-310, 15-317, or 21-300) or permission of the instructor. Some programming background (ideally a course in functional programming like 15-150) is desirable.
If you have any questions as to whether this course is right for you, please do not hesitate to email the instructor.