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:

• Using programs (interactive theorem provers) to
  • verify proofs of results
  • help in generating proofs
• Proving correctness of programs
• Writing programs to find and/or verify proofs
• Functional Programming in Lean

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

• Dependent Type Theory (DTT): foundations used by Lean that include both proofs and computations in a unified way.
• Classical foundations:
  • First-order logic: the usual foundations of mathematics.
  • lambda-calculus: one of the equivalent formulations of the usual foundations of computation.

Prerequisites

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

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

• Instructor: Siddhartha Gadgil
• E-mail: siddhartha.gadgil@gmail.com
• Office: N-15, Department of Mathematics, IISc.
• Timing: Monday, Wednesday, Friday, 9:00-10:00 AM IST
• Venue: LH-3 (ground floor), Department of Mathematics, IISc.
• First meeting: Wednesday, January 4, 2023

Grading

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

• Lab assignments: 20%; these will be regularly assigned.
• Midterm Project: 30%; this will be due at the start of the midterm week.
• Final Project: 50%; this will be due on the date of the final examination.

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 proofs-and-programs-2023.c691c1d30e6095cd0e45e3fb4929734d.show-sender@streams.zulipchat.com.

References

• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4, available at https://leanprover.github.io/theorem_proving_in_lean4/

• Jeremy Avigad, Marijn Heule, Wojciech Nawrocki, Logic and Mechanical Reasoning, available at https://avigad.github.io/lamr/

• Jeremy Avigad, Mathematical Logic and Computation, Cambridge University Press 2022

• Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/