JMM 2027 Tutorial - Lean, AI, and the Future of Mathematical Proof: A Hands-On Tutorial from ICARM

Since the early twentieth century, it has been understood that mathematical definitions, theorems, and proofs can be formalized—that is, expressed in symbolic languages governed by precise rules. In principle, this makes it possible for computers to verify the correctness of mathematical proofs. Today, that possibility has become a practical reality. Using computational proof assistants, mathematicians can write definitions, theorems, and proofs in formal languages that are processed and checked by a computer. In recent years, several high-profile collaborative projects have demonstrated the growing power and relevance of formalization, particularly using the proof assistant Lean. These include the Liquid Tensor Experiment, a formalization of the proof of the polynomial Freiman–Ruzsa conjecture, and a formalization of the optimality of the E8 and Leech lattice sphere packings in eight and twenty-four dimensions, respectively.

Lean’s mathematical library, Mathlib, now contains more than two million lines of formalized mathematics. These examples illustrate that formalization is valuable not only for verification but also for collaboration and the creation of shared mathematical infrastructure. It also offers new opportunities for research, exposition, and teaching, while enabling the use of symbolic and machine-learning-based automation. At the same time, AI systems are rapidly improving in their ability to assist with theorem proving, both formal and informal. These systems often combine language models, search, and proof assistants. The mathematical community is still determining how best to use these tools productively and responsibly.

This workshop will provide an accessible introduction to Lean and related AI systems. Participants will learn how to use Lean, read and write definitions and proofs, navigate Mathlib, and make effective use of emerging AI tools for formalization. We will also discuss current limitations, common pitfalls, and practical workflows.

Our goal is to give participants a realistic understanding of what these technologies can and cannot yet do, and how they may support mathematical work. Participants should bring laptops. No prior experience with Lean or proof assistants is required, though we encourage attendees to explore community resources in advance.

This tutorial is part of the Joint Mathematics Meetings Professional Enhancement Programs. You need to register when you register for the JMM.