The Existential Risk of Mathematical Error
gwern.net
gwern.net
Lounesto was a controversial and sometimes reviled figure, but I (purely as a non-mathematician and sometime reader of his posts) was very sorry to hear of his death in a swimming incident about 10 years ago now. Nice that his website is still available though.
I tend to agree with his idea that it's valuable to search for counterexamples to newer proofs - a sort of application of Popperian principles in the mathematical domain I suppose. I've no idea on the validity of his claims about specific counterexamples, though.
The whole thing (http://www.fantasticmetropolis.com/i/division/full) seems to be temporarily offline, but here's a pretty good summary: http://kasmana.people.cofc.edu/MATHFICT/mfview.php?callnumbe...
> We can probably add software to that list: early software engineering work found that, dismayingly, bug rates seem to be simply a function of lines of code, and one would expect diseconomies of scale. So one would expect that in going from the ~4,000 lines of code of the Microsoft DOS operating system kernel to the ~50,000,000 lines of code in Windows Server 2003 (with full systems of applications and libraries being even larger: the comprehensive Debian repository in 2007 contained ~323,551,126 lines of code) that the number of active bugs at any time would be… fairly large. This lead to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages
Of course, you need to be pretty confident in your proof-checker. If we aren't totally sure about machine-proof methods, then we comback to the "Doomsday hypothesis" at the end of the article, where many results are invalidated at once.
The other issue is usability. Coq is awesome, but proving something more complicated than basic arithmetic results is hard to do. Likewise with ACL2, PVS, and similar systems. It is getting better, but we are still not quite there.
[1] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/
"In some respects, there is nothing to be said; in other respects, there is much to be said" Please edit your blog posts to remove phrases like this which damage reading comprehension. Your opening sentence "Mathematical error has been rarely examined except as a possibility and motivating reason for research into formal methods" is long winded, vague, boring, and tells me nothing about what this post is about.
I think you can write much shorter, clearer articles that are not dense, rambling and inaccessible if you put some time into organization and structure and read your blog critically from a layman's perspective.
There is a limit, were the author is hiding emptiness and sterility behind artificial obscurity and complexity, but I'd say this article is far from that.
> and read your blog critically from a layman's perspective.
Average everyday "laymen" who get brain tired after the first paragraph are almost certainly not the intended audience. I think he's writing to people who will read and think and digest and understand, who enjoy being challenged, and who probably have some background or context on the subject.
I think you know that is very difficult for anyone to do. What has been learned cannot be completely forgotten, and after long enough you no longer remember even vaguely what "a layman's perspective" looks like. This is why writers need copyeditors and beta readers, but unfortunately I have neither.