2 ms·
> He's also excited about the prospect of most math papers publishing machine-checked proofs. Apparently the feels he can't be sure of the correctness of his o
by nova 12y ago
> He's also excited about the prospect of most math papers publishing machine-checked proofs.
Apparently the feels he can't be sure of the correctness of his own papers without machine checked proofs anymore, and he's a Fields medal winner:
I now do my mathematics with a proof assistant and do not have to worry
all the time about mistakes in my arguments or about how to convince
others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the
program remains. Sooner or later computer proof assistants will become
the norm, but the longer this process takes the more misery associated
with mistakes and with unnecessary self-verification the practitioners of the
field will have to endure
(from this http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...)
- dvanduzer 12y agoVladimir Voevodsky may feel that way, but we were talking about Keith Devlin. To answer gre's question, 1994 is the year Devlin cites a major breakthrough in the four color problem, in the very link that gre cited as an example of Devlin's lack of enthusiasm about machine checked proofs. There are plenty of good reasons to mistrust machines when it comes to mathematical proofs, and mathematicians have been correct in their skepticism. Most of the work in Univalent Foundations has been directly aimed at addressing that skepticism. Optimism from its proponents in the 2010s is just as valid as the skepticism in the 70s and 90s. And I mean just as valid in a very specific way; specifically in the spirit of the originally linked Devlin post published today.