Lean - Can we Trust the Trust Engine?

The de Bruin principle - it's all in the Kernel

Once upon a time, in the 1960s, a computer scientist called de Bruijn build a system called Automath. His full name as Nicolaas Govert de Bruijn. It incorporated ideas such as dependent types to make it work.

We call him here a computer scientist, but he can equally be called a mathematician, having made contributions to number theory, analysis, combinatorics and logic, and served as Professor of Mathematics at the University of Amsterdam.

One of the things he studied were sequences now known as de Bruijn sequences. Polish programmer Andrzej Trybulec's Mizar system was influenced by Automath.

De Bruijn came up with the idea of creating a kernel separate from the rest of his system.  This kernel is correctness-validation component of the system - the "rule-checker" if you will. It is like the part of a chess computer that validates legal moves - rather than makes smart moves.

Keeping the kernel separate is known as the de Bruijn principle, joining lots of other artefacts attached to his name (such as the de Bruijn-Newman constant, which is closely associated with the Riemann hypothesis).

What underlying logic to use for the Kernel?

"First order" logic, augmented with axioms of set theory, can serve as a good starting point for a theorem prover/correctness checker.   This approach results in a small kernel but lots of coding for complex mathematics. More complex underlying systems are available, including Higher Order Logic (HOL) and Calculus of Inductive Constructions (CIC). Lean uses the latter, or at least features of the latter, to increase expressivity and make programming easier. Features used include proof irrelevance, quotients and nested inductive types.

Taking one example: proof irrelevance is the principle that given a proposition and any two proofs of the same, the two proofs are (considered) equal. This simplifies type theoretic reasoning.

The result is that Lean has a kernel that is much smaller than Lean itself but verifying it is not trivial.

lean4lean and the "multiple kernel" principle

Creator of Lean, L. de Moura, has advocated the "multiple kernel" principle, strengthening the de Bruijn principle by supporting multiple independent kernels.  Lean 3 thus had three independent kernels, one in Lean, one in Haskell and one in Scala (trepplein). Lean 4 invalidated these kernels. Nanoda, an independent kernel in Rust, was thus commissioned together with procedures to write more kernels.

lean4lean was started by Mario Carneiro, an implementation of Lean in Lean which includes an independent kernel.  Efforts are ongoing to verify kernel correctness.