Seminars & Colloquia Calendar

Abstract: Interactive proof assistants (such as Coq, Isabelle and Lean) feature a formal language for expressing mathematical statements, and collections of "tactics" for building proofs of these statements, down to the axioms. In addition to their potential research application, these systems hold great promise for making mathematics teaching more rigorous.
I will discuss experiments in using the system Lean as an optional supplement to undergraduate mathematics teaching, in real analysis and more recently in intro-to-proof. I will particularly consider the question of how to minimize the difference between the mainstream and formal parts of a course: by careful selection of subject matter, by custom automation of common argument types, and by encouraging particular stylistic patterns in both informal and formal proof.