Comment by QuesnayJr
The specific example of Fermat's Last Theorem is probably true simply because so much work has been done on the modularity of elliptic curves since then, but the probability of false results being proven is much higher than 0%.
In fact, Buzzard has an "existence theorem" of this exact thing. Annals of Mathematics (one of the top mathematics journals) has published one paper proving a theorem, and another paper proving the opposite result of a theorem: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...
My claim is not that nobody ever makes mistakes, it’s formalizing in a computer is extremely high cost for very little reward and doesn’t help the core process of finding proof ideas