Interactive Theorem Proving

Course: 80-419/719, Spring 2019
Instructor: Jeremy Avigad (avigad@cmu.edu)
Time: MW 1:30-2:50

Course Description

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:

  • Dependent type theory
  • Proof terms and tactics
  • Equational reasoning
  • Inductively defined types
  • Type classes
  • Building an algebraic hierarchy
  • Metaprogramming
  • Decision procedures and automation
The emphasis will be on formally verified mathematics, but students will be able to explore topics in hardware and software verification as well.

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.

Prerequisites

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.