Comment by michael0church

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.