Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.
replythat's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.
reply