2.3. Why should we trust Lean?🔗

Now that we have described the way in which a result is considered proved in Lean, it makes sense to ask the question: why should we trust Lean's type inference? What guarantees do we have that the proofs Lean accepts are really correct?

As we have pointed out, proving a result in Lean consists of correctly constructing a term that has a certain type. This process is analogous to verifying programs: it is a matter of checking that a term is well formed (following concrete rules) and satisfies a given specification, expressed as a type. This task falls to Lean's kernel, a small program that contains the minimal implementation of Lean's internal logic.

The remaining components of Lean that we interact with to build proofs (such as the tactics we will see later) return constructions expressed in the language of the Lean kernel (Christopher A. Bailey and Lean community contributors, 2024)Christopher A. Bailey and Lean community contributors, 2024. “Type Checking in Lean 4”. Last accessed: April 23, 2025.. This means that trusting Lean really comes down to trusting its kernelThis idea is known as the de Bruijn criterion, which proposes that a formal verifier should produce its proofs in the language of a small kernel, even if other, more complicated methods are used to construct those proofs in the first place (Christopher A. Bailey and Lean community contributors, 2024. “Type Checking in Lean 4”. Last accessed: April 23, 2025.)..

Now, why do we trust Lean's kernel? Thanks to the kernel being small and isolated from the rest of the system, it is possible to write independent implementations of it that autonomously verify the proofs accepted by Lean. Lean allows these proofs to be exported in an intermediate format that contains all the information needed to reconstruct and validate them externally. Moreover, since this format is modular, it is possible to validate only certain specific aspects of the kernel (Christopher A. Bailey and Lean community contributors, 2024)Christopher A. Bailey and Lean community contributors, 2024. “Type Checking in Lean 4”. Last accessed: April 23, 2025.. For example, Carneiro (Mario Carneiro, 2024)Mario Carneiro, 2024. “Lean4Lean: Towards a formalized metatheory for the Lean theorem prover”. arXiv e-prints, arXiv:2403. describes a new external implementation of the Lean 4 type checker, written in the Lean language itself and capable of verifying the whole Mathlib library.