In addition to what others added below you might be interested in this postmortem https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

You can’t, so you keep the kernel small. The Lean tactics language is rich, so users can autogenerate proofs for the truly trivial bits, but the core language is checkable in dependent type theory.

Kernel bugs, like compiler bugs, exist. As of now, a prover is considered good if it has no known bugs that would thwart a mathematician working in good faith. It’s not considered responsible yet for being impervious to adverse users, but that may change in the age of Ai.

You can only do so in another framework that might itself have bugs.

Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".

The kernel does have bugs sometimes.

You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of?

https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")