Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?
https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")
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.