I fully expect that future programs for formalizing mathematics will reveal that most sufficiently complex proofs are riddled with gaps and errors, and that some of them actually led to false results.

Annals of Mathematics once published a supposed proof (related to intersection bodies IIRC) for a statement that turned out to be false, and it was discovered only by someone else proving the opposite, not by someone finding an error.