The Lean proof assistant is seeing increasing use in mathematics formalization and software verification, but the metatheory of Lean is not yet completely understood. In particular, while there is an intended interpretation within a classical set-theoretical model, the proof of soundness has not been formalized. The Lean4Lean project endeavors to verify the key theorems (and non-theorems!) of the LeanTT formal system. Additionally, Lean4Lean provides an executable typechecker, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean’s Mathlib library, forming an additional step in Lean’s aim to self-host the full elaborator and compiler. Ultimately, we plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs.

In this talk, I will present the latest progress in Lean4Lean, including verification of large parts of the typechecker, as well as some open problems in the metatheory and a roadmap for the rest of the project and how people can get involved.

Bio: Mario is a postdoc at Chalmers University of Technology (Sweden). He has been working with ITPs since 2013, first in Metamath, then in Lean, and is a founder and maintainer of the Mathlib Lean library. He now works on theorem prover design and proof translation, with experience in a wide variety of other proof assistants including Rocq, Agda, HOL Light, Isabelle, HOL4, and Mizar. His PhD (at CMU, advised by Jeremy Avigad) introduced the Metamath Zero ITP, a minimalistic language which can verify the machine code of a proof checker for itself. If you find him in the hallway, he’s happy to chat about expressive type systems for low level languages, and type checker performance techniques. He is also interested in linguistics and learns languages as a hobby.