Re:New math book rescues landmark topology proof
by ouid on Thursday September 09, 2021 @04:03PM
(#28474029)
> 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.
Adding to this problem the intersection of mathematicians who understand computer aided verification and who understand a particular piece of research mathematics is often empty, and even if there are a handful of people who could do the necessary work they're often busy doing more interesting stuff.
Finally I don't think a big proof that has been accepted by the community has ever been found to be false by programmatic methods. I think its unlikely that this will happen for a long time, for the simple reason that to feed a proof into a computer requires someone to dissect the proof to its logical bare bones in the first place, and the person doing the dissection is likely to notice any errors before they get round to feeding the problem into the computer.