MA 208: Proofs and Programs

Credits: 3:1


This course introduces various aspects of Computer Proofs, both interactive and fully automated. We will consider proofs of mathematical results as well as of correctness of programs. We will primarily use the Lean Theorem Prover 4, which is a formal proof system as well as a programming language. The foundations on which the Lean prover is based, Dependent Type Theory, allow a seamless integration of mathematical objects, theorems, proofs and algorithms.

Topics covered will be among the following.


Suggested books and references:

  1. 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/.
  2. Jeremy Avigad, Marijn Heule, Wojciech Nawrocki, Logic and Mechanical Reasoning, available at https://avigad.github.io/lamr/.
  3. Jeremy Avigad, Mathematical Logic and Computation, Cambridge University Press 2022.
  4. Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/.

All Courses


Contact: +91 (80) 2293 2711, +91 (80) 2293 2265 ;     E-mail: chair.math[at]iisc[dot]ac[dot]in
Last updated: 09 Dec 2022