The Existential Risk of Mathematical Error

http://www.gwern.net/The%20Existential%20Risk%20of%20Mathematical%20Error

by gwern • 13 years ago

106 20 13 years ago

gwern.net

consider_this• 13 years ago

"This sentence is false".

mjcohen• 13 years ago

This sentence is not.

Bakkot• 13 years ago

No mention of machine proof? Surely those raise the upper bound on our confidence in a new result significantly.

tribe• 13 years ago

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.

betterunix• 13 years ago

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.

kvb• 13 years ago

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/

elliotlai• 13 years ago

Agda!

ttctciyf• 13 years ago

Reminds me of the late lamented Pertti Lounesto who made himself quite unpopular by looking for counterexamples to some accepted proofs and posting about them repeatedly on Usenet. See http://users.tkk.fi/ppuska/mirror/Lounesto/counterexamples.h... for example.

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.

onosendai• 13 years ago

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

majormajor• 13 years ago

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

sxp• 13 years ago

http://web.archive.org/web/20130112204225/http://www.fantast... has a backup.

MasterScrat• 13 years ago

Fiction! it's a fiction. I didn't realize until after I finished. For some reason I feel better now.

nitrogen• 13 years ago

On the subject of mathematical fiction, the story of the secret number bleem is interesting: http://www.strangehorizons.com/2000/20001120/secret_number.s...

AlexDanger• 13 years ago

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.

yOutely• 13 years ago

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.

JamesArgo• 13 years ago

That quote makes sense enough in context.

gbog• 13 years ago

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.

adrianN• 13 years ago

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.

SkyMarshal• 13 years ago

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.

gwern• 13 years ago

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.

The Existential Risk of Mathematical Error

Related Stories