Taught by Anthony Wang
Tired of debugging bad code? Interested in weird programming languages? Curious about using computers for doing math? In this fast-paced not-for-credit class, we'll learn the Lean programming language, which is probably radically different from any other language you've used before. We'll explore some of Lean's powerful features, such as dependent types, type classes, monads, local imperativity, and tactics. Hopefully, this class will give you a fresh new perspective on an alternative way of programming and doing math.
Prereqs: 6.101 or equivalent, 6.120 or equivalent
Compared to 6.S057 Verified Software Engineering: 6.S057 uses the Dafny automated theorem prover which has a long history of serious bugs. Don't use Dafny, it's unsound!
Compared to 6.512 Formal Reasoning About Programs: 6.512 uses Rocq instead of Lean. I haven't actually taken it, but my friend said that class mostly just proves trivial things. This class will try to prove some nontrivial theorems too, using Lean's Mathlib library and modern automated tactics like grind.
Location and time: 6-7:30 PM, 3-370
Office hours: 3-5 PM, Jan 19, 22, 26, W20-557 (SIPB office)
| Date | Lecture | Description (tentative) | Pset |
|---|---|---|---|
| Jan 16 | Why Lean? | Cool Lean projects, history of proof assistants, ITPs vs ATPs, propositional logic, Curry-Howard, simply typed lambda calculus, first-order logic, dependent type theory, calculus of constructions, pure type systems | Pset1.lean |
| Jan 20 | Basic Topics |
Induction (recursion), inductive types, pattern matching, polymorphism, termination checking, type classes, functors, applicatives, monads, do notation, IO, vectors, indexing proofs, tactics for basic logic, grind, Loogle
|
Pset2.lean |
| Jan 23 | Advanced Topics |
Universes, Prop weirdness, choice, subtypes, quotients, algebraic hierarchies in Mathlib, mvcgen, Hoare triples, denotational semantics
|
Pset3.lean |