Mathematics in Lean (Summer 2026 Session 2) will discuss how to teach mathematics to a computer.
You might be asking yourself right now why anyone would want to teach mathematics a computer. One compelling answer was giving in 2020 by Fields Medalist Peter Scholze, through the Liquid Tensor Experiment. At the time, Scholze had just completed what he considered the most difficult proof of his career. Yet the arguments were so intricate that he was not entirely convinced that all the steps were correct. Since he had exhausted all traditional verification methods, he asked the Lean community to formally verify the proof by translating it into a computer program—the Lean4 proof assistant.
The goal of this course is to understand what a proof assistant is, how it works, and how to use it effectively. In short, we’re going to learn about formal proof verification. Along the way, we will revisit the fundamental proof concepts introduced in the Transition to Proofs class, deepen our understanding of the logical structure of mathematical arguments, and ultimately formally verify a well-known theorem.
The structure of this class is slightly unconventional. In the first half, we will focus on learning the fundamentals of formal verification. The second half will be devoted to a collaborative project, though not in the traditional sense. The structure of Lean allows students to work independently on well-defined pieces of the puzzle, which are then combined into a single fully verified proof. This style of collaboration is often cited as a prototype for the future of mathematical research, as advocated by influential mathematicians such as Kevin Buzzard and Terence Tao.
Prerequisites:
- An understanding of proofs at the level of the Transition to Proofs class (proof by contradiction, induction, axioms, definitions, and theorems)
- Basic number theory and knowledge of real numbers, functions, and limits
- Access to a computer with Visual Studio Code
P.S.: The Liquid Tensor experiment was a success! After several years of work, the theorem in question, along with many other theorems, was finally verified using the Lean4 proof assistant.
This class will run for 5 weeks, from July 13 through August 14, meeting Mondays, Tuesdays, Thursdays, and Fridays from 9:30–11:30 AM Pacific time. There may be additional optional (but strongly encouraged) sessions at other times. Students will be expected to do a considerable amount of work outside of class; this is expected to be the students’ primary activity for the duration of the class. The class will primarily be held on Zoom, but we may schedule optional extra in-person sessions for local students if there is sufficient interest.
Applications for this class are due April 12. Click here to apply!
Euler Circle 