The mathematician and Fields medalist Vladimir Voevodsky on using automated proof assistants in mathematics:
[Following the discovery of some errors in his earlier work:] I think it was at this moment that I largely stopped doing what is called “curiosity driven research” and started to think seriously about the future.
[...]
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.
[...]
Among mathematicians computer proof verification was almost a forbidden subject. A conversation started about the need for computer proof assistants would invariably drift to the Goedel Incompleteness Theorem (which has nothing to do with the actual problem) or to one or two cases of verification of already existing proofs, which were used only to demonstrate how impractical the whole idea was.
[...]
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.
From a March 26, 2014 talk. Slides available here.
Computer scientists seem much more ready to adopt the language of homotopy type theory than homotopy theorists at the moment. It should be noted that there are many competing new languages for expressing the insights garnered by infinity groupoids. Though Voevodsky’s language is the only one that has any connection to computers, the competing language of quasi-categories is more popular.
The mathematician and Fields medalist Vladimir Voevodsky on using automated proof assistants in mathematics:
[...]
[...]
[...]
[...]
From a March 26, 2014 talk. Slides available here.
A video of the whole talk is available here.
And his textbook on the new univalent foundations of mathematics in homotopy type theory is here.
It is misleading to attribute that book solely to Voevodsky.
Yes. But it’s forgiveably misleading to attribute it non-exclusively to him, in a thread of comments which was started about him.
Computer scientists seem much more ready to adopt the language of homotopy type theory than homotopy theorists at the moment. It should be noted that there are many competing new languages for expressing the insights garnered by infinity groupoids. Though Voevodsky’s language is the only one that has any connection to computers, the competing language of quasi-categories is more popular.
I know you’re not supposed to quote yourself, but I came up with a cool saying about this a while back and I just want to share it.
Computer proof verification is like taking off and nuking the whole site from orbit: it’s the only way to be sure.