Ian Jauslin

Formalizing mathematics with Lean and Mathlib

DIMACS, Rutgers University, New Jersey, USA

July 1, 2025

Math is hard. And mathematicians are human. This has lead to various high profile instances of published theorems being found to be incorrect, or incomplete. But even beyond such rare events, the main medium mathematicians use to write out their results are research papers, which mainly serve the purpose of disseminating proofs, and are thus mainly a tool of communication. The peer review process provides a guarantee that the result is correct, but one cannot expect referees to do a perfect job of verifying every detail. At any rate, this would be impossible: no published paper contains all the pre-requisites needed to verify its proofs. To obtain an iron-clad guarantee that a result is correct and complete, a number of computer-based proof verification software systems have been designed over the past few decades.

In this talk, I will present one such software package, called Lean, which was designed to be more user-friendly than other languages, and has received much attention from the mathematics community over the past decade. Over this time, a large library of results, formalized in Lean, has been compiled, and can be used to formalize and verify even difficult, research-level mathematics. In this talk, after a brief overview of the history and the motivations for formalized proof verification, I will give a short tutorial on installing and using Lean, and then discuss an example of formalizing a simple result, and proving it with Lean.

Links

Slides


webmaster