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:
 Firstorder logic: the usual foundations of mathematics.
 lambdacalculus: 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.
 Lab 01: Setup due by Monday, Jan 30, 2023.
 Lab02: Selection Sort (part 1) and `≤` on `Answer` due by Monday, Feb 6, 2023.
 Lab03 Selection Sort (part 2) due by Monday, Feb 13, 2023.
 Vectors: Equivalence of definitions due by Monday, Mar 20, 2023.
Course Details
 Instructor: Siddhartha Gadgil
 Email: siddhartha.gadgil@gmail.com
 Office: N15, Department of Mathematics, IISc.
 Timing: Monday, Wednesday, Friday, 9:0010:00 AM IST
 Venue: LH3 (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 assigments: 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 proofsandprograms2023.c691c1d30e6095cd0e45e3fb4929734d.showsender@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/