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.