The Existential Risk of Mathematical Error(gwern.net)
gwern.net
The Existential Risk of Mathematical Error
http://www.gwern.net/The%20Existential%20Risk%20of%20Mathematical%20Error
20 comments
This reminds me of an excellent short story by Ted Chiang, "Division by Zero", which deals with a mathematician's deteriorating mental state and attempted suicide as a consequence of proving the inconsistency of mathematics.
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...
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...
That story is in Stories of Your Life and Others; I'd recommend the whole collection: http://www.amazon.com/Stories-Your-Life-Others-Chiang/dp/193...
Fiction! it's a fiction. I didn't realize until after I finished. For some reason I feel better now.
On the subject of mathematical fiction, the story of the secret number bleem is interesting: http://www.strangehorizons.com/2000/20001120/secret_number.s...
No mention of machine proof? Surely those raise the upper bound on our confidence in a new result significantly.
What machine proofs do is concentrate the risk of errors on the proof checker. That is great if your proof checker is reliable, and catastrophic if it is unreliable. Fortunately, proof checkers need not be complicated; you only need a small kernel, from which you can build the rest of the theory.
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.
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.
It's hard to do, but it is being done. See e.g. Gonthier's celebrated work formalizing the Feit-Thompson theorem[1].
[1] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/
[1] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/
Well there was some mention.
> 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.
> 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.
Great article, and I highly recommend the rest of the articles on gwern.net if you're looking for thought provoking and well-researched writing on a range of topics.
Agda!
What is this blog and why is it getting popular? The articles are very long and dense with no clear point.
"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.
"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.
Pro-tip: HN articles are about 90% noise, 10% signal. Gwern.net is among the latter.
> 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.
> 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.
You know, sometime some thought do actually require sentences with more than five words, and some people might actually appreciate rich and flourishing vocabularies. See Proust.
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.
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.
Yes, some arguments require complicated reasoning. However, even in such cases the author still is responsible for keeping the reader's interest. For this it is for example helpful to start with an introduction to the topic and end with a summary. Writing is also better if it doesn't contain phrases that add little to nothing to the content.
> 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.
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.
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.
That quote makes sense enough in context.
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.