3 ms·

The problem is, once you have a proof that everyone agrees is correct, what's the incentive to painstakingly translate it into something a computer also agrees

The problem is, once you have a proof that everyone agrees is correct, what's the incentive to painstakingly translate it into something a computer also agrees is correct? Yes, you might turn up some "bugs" in the proof, but proof bugs can almost always be ironed out. It's a very rare proof that is accepted and then falls apart later. If proofs were as "buggy" as computer programs- falling apart all the time- then there'd be a much bigger appetite for proof checkers. But as it is, mathematical peer review seems to work awfully well.

mahogany 5y ago
I agree that it's rare that a proof is accepted and falls apart later, but it does happen occasionally. Somewhat famously, Voevodsky turned his attention to mathematical foundations, including proof assistants, at least in part because he was spooked that a part in one of his big papers was later shown to be incorrect. (Interestingly, someone much less known pointed this out in a preprint but it was, from my memory, largely ignored for some time -- who's going to believe a nobody versus a Fields Medalist?) There's a talk that Voevodsky gives at (I think) IAS, where he mentions this. --- Edit: okay, here are the slides: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio... The whole talk is interesting, but slides 8-13 talk about the topic at hand. In particular: > This story got me scared. Starting from 1993 multiple groups of mathematicians studied the “Cohomological Theory” paper at seminars and used it in their work and none of them noticed the mistake. > And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail. ... > It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.
zozbot234 5y ago
There's plenty of incentive to do that actually, since a translation of a proof that had not been formalized before yields a much clearer proof than anything a human could write on her own. This is doubly true when some "bugs" are found and "ironed out" in the process - even seemingly trivial bugs can trip up the reader and obscure interesting sr structure. In fact, a truly novel formalization is pretty much publishable work in and of itself. The problem is not incentives; it's more of a lack of willingness to work in an area that's very fragmented still and makes it way too hard to reuse existing results.

mahogany 5y ago

I agree that it's rare that a proof is accepted and falls apart later, but it does happen occasionally. Somewhat famously, Voevodsky turned his attention to mathematical foundations, including proof assistants, at least in part because he was spooked that a part in one of his big papers was later shown to be incorrect. (Interestingly, someone much less known pointed this out in a preprint but it was, from my memory, largely ignored for some time -- who's going to believe a nobody versus a Fields Medalist?) There's a talk that Voevodsky gives at (I think) IAS, where he mentions this. --- Edit: okay, here are the slides: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundatio... The whole talk is interesting, but slides 8-13 talk about the topic at hand. In particular: > This story got me scared. Starting from 1993 multiple groups of mathematicians studied the “Cohomological Theory” paper at seminars and used it in their work and none of them noticed the mistake. > And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail. ... > It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.

zozbot234 5y ago

There's plenty of incentive to do that actually, since a translation of a proof that had not been formalized before yields a much clearer proof than anything a human could write on her own. This is doubly true when some "bugs" are found and "ironed out" in the process - even seemingly trivial bugs can trip up the reader and obscure interesting sr structure. In fact, a truly novel formalization is pretty much publishable work in and of itself. The problem is not incentives; it's more of a lack of willingness to work in an area that's very fragmented still and makes it way too hard to reuse existing results.