Interactive Theorem Proving

Catalog description

Interactive theorem proving involves using computational proof assistants to verify that mathematical proofs are correct, or to verify that hardware and software designs meet their formal specifications. This course uses a new interactive theorem prover, Lean, to explore this new technology and its logical foundations. We will study dependent type theory, a powerful and expressive language for representing mathematical objects, algorithms, and proofs. We will also consider automated methods that can be used in support of formal verification, including propositional, equational, first-order, and higher-order methods, as well as decision procedures for real and integer arithmetic. Prerequisites: 80-211 or 80-310 or 15-317 or 21-300 Course Website: https://leanprover.github.io/theorem_proving_in_lean/