Trust in formal reasoning is necessarily always conditional. You have to start somewhere. The good thing about verified formal proofs is that the only way they can be in error is if the verifier is faulty. This drastically limits the possible reasons for error.

(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)

One can only trust a verifier as far as they can trust anything made out of software.

It has nothing to do with LLMs. One cannot trust the proof of anything if one cannot trust the verifier.

I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell.

That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.