Tired of debugging bad code? Interested in weird programming languages? Curious about using computers for doing math? In this 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 and quirky features, such as first-class types, type classes, monads, local mutability, and tactics. Hopefully, this class will give you a fresh new perspective on an alternative way of programming and doing math.