That's not how it works. If you input garbage in Lean or other proof checker they will just tell you it's wrong. You would have to input garbage in the statemen

That's not how it works. If you input garbage in Lean or other proof checker they will just tell you it's wrong. You would have to input garbage in the statement you want to prove for them to accept a wrong proof (which must still be correct for that garbage statement!). To rule this out you just have to manually check the translation of the statement, which is most often much much smaller than the proof itself.