The main issue would rather that the formalization itself has a bug, eg. those proofs that you're trying to formalize are not "1 + 1 = 2" but theorems which take already multiple pages just to enunciate. And in these enunciations (that are made by humans) there can be errors.

In general, once the proof has been formalized, it's supposed to be the proof of the correct theorem (that's what the Lean proof-checker checks)