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
Fully automated theorem proving: SAT Solvers, Resolution Theorem Proving etc.
Use of Machine Learning in Automated and Interactive Theorem Proving.