3.0

Average Course Rating

Over millennia, mathematicians have developed an increasingly precise system of logical reasoning which determines what counts as a valid proof of a mathematical statement. But pen-and-paper proofs can contain subtle mistakes that are hard to catch. This First-Year Seminar will provide a hands-on introduction to a new method of proof writing, where a logical argument is developed interactively with a computer tool called a computer proof assistant, which simultaneously checks the underlying logic. Through a series of games, we'll explore the computer proof assistant Lean while learning how to state, interpret, and prove increasingly sophisticated theorems. The course will also discuss real-world applications of "formal methods" to verifying software and hardware as well as the effect this paradigm-shifting method of proof-writing is having on mathematical research.