1. Terms and Proofs (21/1/2025).
  2. Recursion (30/1/2025).
  3. Inductive Types; Typeclasses (25/2/2025).

MA 208: Proofs and Programs

January 2025

This course is an introduction to interactive theorem proving using the proof assistant Lean. Interactive theorem proving can be used to formalize mathematics and to verify the correctness of programs. We will discuss both aspects in this course.

Formalizing mathematics in Lean involves stating and proving mathematical results, with Lean checking the correctness of the proofs as well as assisting in completion of the proofs. This not only guarantees the correctness of the results but also facilitates large-scale collaboration and the use of computer algebra systems, as trust is much less of an issue than in pen-and-paper mathematics. Formalizing a results also forces one to be precise about definitions and assumptions, which can lead to a deeper understanding of the mathematics.

Lean can also be viewed as a programming language. From this viwepoint it is pleasant and fast – indeed fast enough that Lean is mostly written in Lean. It has a type system that is rich enough to formalize all of mathematics, allowing functions to be defined in such a way that the compiler can check that they are correct by construction. This is a powerful tool for writing correct programs, and for verifying that they are correct. Indeed, this course can also be viewed as an introduction to functional programming in Lean.

While this course will not involve AI/ML directly, in many ways Interactive Theorem Proving perfectly complements Deep Learning, in particular Generative AI. Generative AI is powerful but unreliable, so combining with Interactive Theorem Proving allows checking the results of Generative AI. Indeed many systems, such as AlphaProof, combine Deep Learning and Interactive Theorem Proving.

Prerequisites

The only prerequisites for this course are:

In particular, no knowledge of Lean of formal logic is required.

Assignments

Assignments will be posted roughly once a week. These will be lab assignments where you write Lean proofs/code.

  1. Terms and Proofs due by Tuesday, Jan 21, 2025.
  2. Recursion due by Thursday, Jan 30, 2025.
  3. Inductive Types; Typeclasses due by Tuesday, Feb 25, 2025.

Course Details

Projects

A core component of the course is the project. This can be done individually or in groups. However, while a project is “owned” by a group or individual, collaborative live-coding will be done in lectures on projects with everyone contributing. Indeed, many concepts will be explained and illustrates through code relevant to the projects.

The projects will be Lean code which can be either implementations of algorithms with proofs in Lean or formalizations of mathematical results in Lean. There is considerable flexibility in the choice of projects. However, the topic of the project must be chosen to be useful to the Lean ecosystem, so should avoid dulicating existing code. Further, all code must be properly documented.

Grading

Course grades will be based on labs, a midterm examination, and the final project. The weights are as follows:

Setting up Lean 4 and Repository

For details on setting up Lean 4 and repositories for assignments and projects, see the Lean setup instructions.

Zulip chat

As with Lean we will use a Zulip server for discussions. You can also post on the stream by sending an email to the channel address.

References