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.
- Interactively proving mathematical results in the lean theorem prover.
- Programming in lean - functional programming with dependent types.
- Mathematical proofs of correctness of programs.
- Foundations of Mathematics and Computation using Dependent Type Theory
- First-order logic
- Fully automated theorem proving: SAT Solvers, Resolution Theorem Proving etc.
- Use of Machine Learning in Automated and Interactive Theorem Proving.
Suggested books and 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/.