What Is Your Proof Assistant Actually Checking?

When a theorem is formally verified, the promise being made is the de Bruijn criterion: however elaborate the tooling that produced the proof, the result is rechecked by one small program, the kernel, so that trust in a million-line library reduces to trust in a few thousand lines. It is a good argument. It is also a claim about a specific piece of software, and one worth looking at closely.

 

This talk is a tour of that program: what a kernel has to do, what it deliberately refuses to do, and why the boundary sits where it does. The interesting parts are the ones a textbook presentation leaves out, and they are, not coincidentally, the parts where real kernels have turned out to be unsound. That raises the question of what it would take to be sure, which requires first writing down what a kernel is supposed to do at all.

Lean4Lean is an attempt to do exactly that: a kernel for Lean, written in Lean, together with a formalization of Lean's type theory and a proof that the one meets the other. It began as a solo project, but a steady stream of soundness bugs found in Lean's kernel over the past year has put it in the spotlight, and it is now becoming a collaborative one. I will describe how far it has got, and what it would take to finish.