> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. Right, because that's not how it w

> I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. Right, because that's not how it works. Errors aren't discovered after the proof has been translated into machine language because that is the only step of the verification. As soon as the code is written, the proof is verified. Necessarily, then, any error discovery has to happen before that.