Mathematics 222 - Interactive Theorem Proving

A proof assistant is a computer program that verifies the integrity of mathematical reasoning. Such software addresses an aspiration predating the invention of computers: can we find certainty in our arguments by fully mechanizing them? Rather than writing every detail, the user specifies tactics and techniques to apply, and the software replies with what it could formalize and verify. This course uses a proof assistant called Lean, which is powerful and usable enough to verify theorems at the cutting edge of mathematics research. The course emphasizes how the interactive window provided by Lean can help students learn to write and understand human-written proofs. Students will practice formalizing theorems from a variety of mathematics topics, some of which may be drawn from their other interests and coursework.
 

Fall semester. Professor Pflueger

How to handle overenrollment: Preference given to first and second year students. Math majors and non-majors are welcome.

Students who enroll in this course will likely encounter and be expected to engage in the following intellectual skills, modes of learning, and assessment: May include written problem sets, programming assignments, in-class group work, in-class quizzes or exams, take-home exams, and final projects.