Lean is both a purely functional, dependently-typed programming language and a "proof assistant". Using Lean has been described as "programming proofs". It has been used to: formalize and verify mathematical theorems, distributed computing and cryptographic protocols, hardware models, neural networks, and many other kinds of abstractions; to implement and prove properties of software applications and concrete hardware designs; to model and verify properties of systems built in other languages; and much more.
This course is an introduction to Lean, both as a programming language and as a proof assistant. The goal is to provide a basic foundation that students can use to later explore Lean further for whatever purpose interests them. The course will consist of weekly readings and exercises, and a final project.
Pre-requisites: Students are expected to be familiar with programming (though not necessarily functional programming) and with formal proofs and proof techniques (e.g., proof by cases, proof by contradiction, and proof by induction). The point of Lean is to formalize and prove things, so students should enjoy that kind of activity.
Once the quarter starts, instructor approval is required to maintain enrollment in the course, including if students do not have the listed pre-requisite courses completed.