MA 208: Proof and Programs

January 2023

This course will introduce Lean Theorem Prover 4, which is an interactive theorem prover as well as a programming language and use it for various aspects of proofs and programs:

To study these things in a meaningful way, we will look at foundations of mathematics and of computation. We will introduce different foundational systems:


No background in logic or programming is required. Some mathematical maturity is required: in particular familiarity with proofs. Besides this the only requirements are open mindedness and willingness to spend a (modest amount of) time and effort to setup a working environment and dealing with technical issues.


Assignments will be posted roughly once a week. These will be lab assignments involving programming and/or formal proving in Lean 4.

  1. Lab 01: Setup due by Monday, Jan 30, 2023.
  2. Lab02: Selection Sort (part 1) and `≤` on `Answer` due by Monday, Feb 6, 2023.
  3. Lab03 Selection Sort (part 2) due by Monday, Feb 13, 2023.
  4. Vectors: Equivalence of definitions due by Monday, Mar 20, 2023.

Course Details


Course grades will be based entirely on code in Lean and your knowledge of related concepts, which has three components:

The projects will be Lean code which can be either implementations of algorithms with proofs in Lean or formalizations of mathematical results in Lean. All code must be properly documented. There is considerable flexibility in the choice of projects, including to work collaboratively. The evaluation will be based on both the code itself and presentations of the code. In addition there will be viva sessions where the students show their knowledge of the code and related concepts.

Setting up Lean 4 and Repository

For details on setting up Lean 4 and repositories for assignments and projects, see the 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 address