Course Syllabus

MAT 180 (Prof. Koeppe): Introduction to computer-assisted theorem proving

We will learn about topics related to computer-assisted theorem proving: Logic, foundations, certified computation. We will learn to use a variety of software, including the system Lean
(https://leanprover.github.io/theorem_proving_in_lean/index.html) in combination with mathlib
(https://github.com/leanprover-community/mathlib). Final projects will contribute to the library of theorems with formalized proofs in one of several areas of mathematics.

Professor Köppe teaches this course in synchronous remote instruction mode over Zoom. Attendance is required. No course videos will be provided. 

Required prerequisites

All of the following:

• Command of a programming language
• A course providing an introduction to writing mathematical proofs such as MAT 67 or MAT 108.
• At least one upper division course with a focus on writing mathematical proofs.
• At least one upper division course with a focus on algorithms or computation.
  

Grading

Homework projects and a final project.

For some of the projects, work in small groups will be allowed; details TBA.