Isn't it also possible that the written proofs themselves are incorrect, say, for example, by mis-specification of constraints? Let's say I publish what I claim is a proof that 2+2=4, but in the Lean specification, I proved 1+1=2.

To be pedantic, the proofs would be correct, they would just be proving the wrong thing.

To address what you actually meant: it's possible but specifications are way easier to verify.

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)