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.
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.
Homework projects and a final project.
For some of the projects, work in small groups will be allowed; details TBA.
The syllabus page shows a table-oriented view of the course schedule, and the basics of course grading. You can add any other comments, notes, or thoughts you have about the course structure, course policies or anything else.
To add some comments, click the "Edit" link at the top.