Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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_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.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: