Formalization of Mathematics: Seminar on the proof assistant Lean

The Curry-Howard correspondence between types/programs (in computer science) and propositions/proofs (in mathematics) has led to the development of software - known as 'proof assistants' or 'interactive theorem provers' - that are used to formalize mathematics. This seminar is an introduction to the proof assistant Lean. Students will learn to formalize mathematics in Lean, including: implementation of definitions, encoding propositions, using tactics, and developing mathematics formally. Recommended prerequisite: one of Math 221, 242, or 245 (minimum grade of B suggested for success in this course), or an equivalent rigorous, proof-based mathematics course, and CompSci 101 or equivalent, or by instructor consent.