If there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times.

It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.

There's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/

But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".