Lean4Lean: Verifying a Typechecker for Lean, in Lean

TL;DR

This paper introduces a new Lean-based external typechecker for Lean 4, enabling formal verification of the kernel and improving trustworthiness, while maintaining competitive performance.

Contribution

It presents the first complete Lean 4 typechecker written in Lean, facilitating formal verification and correctness proofs of the kernel.

Findings

Checker is 20-50% slower than the reference implementation.

Able to verify the entire mathlib library.

Identified and fixed a soundness bug.

Abstract

In this paper we present a new "external checker" for the Lean theorem prover, 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. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on progress to formalize the Lean type theory abstractly and prove some theorems about it. Finally, we combine these to get a proof of correctness of parts of the kernel. 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. The verification is already paying off, as one soundness bug has been spotted and fixed as a result of this work.