It really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you!

Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true.

Obviously this only applies to bugs in the implementation as opposed to an unsound logic.