Trust Lean proof?

I see many people claiming you can’t trust a Lean proof because Lean is buggy. I know someone tried to validate a false proof of Collatz by exploiting a bug. I also know that if there is an error in the Lean statements of the theorem or the axioms, the proof will be invalid. Is there any example of a false proof due to a bug or a reason other than the above?