{"id":4133,"date":"2019-03-07T04:11:41","date_gmt":"2019-03-07T10:11:41","guid":{"rendered":"https:\/\/scottaaronson.blog\/?p=4133"},"modified":"2019-09-24T21:21:26","modified_gmt":"2019-09-25T02:21:26","slug":"death-of-proof-greatly-exaggerated","status":"publish","type":"post","link":"https:\/\/scottaaronson.blog\/?p=4133","title":{"rendered":"Death of proof greatly exaggerated"},"content":{"rendered":"\n

In 1993, the science writer John Horgan<\/a>—who’s best known for his book The End of Science<\/a><\/em>, and (of course) for interviewing me in 2016<\/a>—wrote a now-(in)famous cover article for Scientific American<\/em> entitled “The Death of Proof.”<\/a> Mashing together a large number of (what I’d consider) basically separate trends and ideas, Horgan argued that math was undergoing a fundamental change, with traditional deductive proofs being replaced by a combination of non-rigorous numerical simulations, machine-generated proofs, probabilistic and probabilistically-checkable proofs, and proofs using graphics and video. Horgan also suggested that Andrew Wiles’s then-brand-new proof<\/a> of Fermat’s Last Theorem—which might have looked, at first glance, like a spectacular counterexample to the “death of proof” thesis—could be the “last gasp of a dying culture” and a “splendid anachronism.” Apparently, “The Death of Proof” garnered one of the largest volumes of angry mail in Scientific American<\/em>‘s history, with mathematician after mathematician arguing that Horgan had strung together half-digested quotes and vignettes to manufacture a non-story.<\/p>\n\n\n\n

Now Horgan—who you could variously describe as a wonderful sport, or a ham, or a sucker for punishment—has written a 26-year retrospective<\/a> on his “death of proof” article. The prompt for this was Horgan’s recent discovery that, back in the 90s, David Hoffman and Hermann Karcher, two mathematicians annoyed by the “death of proof” article, had named a nonexistent mathematical object after its author. The so-called Horgan surface<\/a><\/em> is a minimal surface that numerical computations strongly suggested should exist, but that can be rigorously proven not to exist after all. “The term was intended as an insult, but I\u2019m honored anyway,” Horgan writes.<\/p>\n\n\n\n

As a followup to his blog post, Horgan then decided to solicit commentary from various people he knew, including yours truly, about “how proofs are faring in an era of increasing computerization.” He wrote, “I’d love to get a paragraph or two from you.” Alas, I didn’t have the time to do as requested, but only to write eight<\/i> paragraphs. So Horgan suggested that I make the result into a post on my own blog, which he’d then link to. Without further ado, then:<\/p>\n\n\n\n

\n\n\n\n

John, I like you so I hate to say it, but the last quarter century has not been kind to your thesis about \u201cthe death of proof\u201d!  Those mathematicians sending you the irate letters had a point: there\u2019s been no fundamental change to mathematics that deserves such a dramatic title.  Proof-based math remains quite healthy, with (e.g.) a solution to the Poincar\u00e9 conjecture<\/a> since your article came out, as well as to the Erd\u0151s discrepancy problem<\/a>, the Kadison-Singer conjecture<\/a>, Catalan\u2019s conjecture<\/a>, bounded gaps in primes<\/a>, testing primality in deterministic polynomial time<\/a>, etc. \u2014 just to pick a few examples from the tiny subset of areas that I know anything about.<\/p>\n\n\n\n

There are evolutionary changes to mathematical practice, as there always have been.  Since 2009, the website MathOverflow<\/a> has let mathematicians query the global hive-mind about an obscure reference or a recalcitrant step in a proof, and get near-instant answers.  Meanwhile \u201cpolymath\u201d projects<\/a> have, with moderate success, tried to harness blogs and other social media to make advances on long-standing open math problems using massive collaborations.<\/p>\n\n\n\n

While humans remain in the driver\u2019s seat, there are persistent efforts to increase the role of computers, with some notable successes.\u00a0 These include Thomas Hales\u2019s 1998 computer-assisted proof of the Kepler Conjecture<\/a> (about the densest possible way to pack oranges) \u2014 now fully machine-verified from start to finish, after the <\/del>Annals of Mathematics<\/del><\/em> refused to publish a mixture of traditional mathematics and computer code<\/del> (seems this is not exactly what happened; see the comment section for more).\u00a0 It also includes William McCune’s 1996 solution to the Robbins Conjecture<\/a> in algebra (the computer-generated proof<\/a> was only half a page, but involved substitutions so strange that for 60 years no human had found them); and at the \u201copposite extreme,\u201d the 2016 solution to the Pythagorean triples problem<\/a> by Marijn Heule and collaborators, which weighed in at 200 terabytes (at that time, \u201cthe longest proof in the history of mathematics\u201d).<\/p>\n\n\n\n

It\u2019s conceivable that someday, computers will replace humans at all aspects of mathematical research \u2014 but it\u2019s also conceivable that, by the time they can do that, they\u2019ll be able to replace humans at music and science journalism and everything else!<\/p>\n\n\n\n

New notions of proof<\/a> \u2014 including probabilistic, interactive, zero-knowledge, and even quantum proofs \u2014 have seen further development by theoretical computer scientists since 1993.  So far, though, these new types of proof remain either entirely theoretical (as with quantum proofs<\/a>), or else they\u2019re used for cryptographic protocols but not for mathematical research.  (For example, zero-knowledge proofs now play a major role in certain cryptocurrencies, such as Zcash<\/a>.)<\/p>\n\n\n\n

In many areas of math (including my own, theoretical computer science), proofs have continued to get longer and harder for any one person to absorb.  This has led some to advocate a split approach, wherein human mathematicians would talk to each other only about the handwavy intuitions and high-level concepts, while the tedious verification of details would be left to computers.  So far, though, the huge investment of time needed to write proofs in machine-checkable format \u2014 for almost no return in new insight \u2014 has prevented this approach\u2019s wide adoption.<\/p>\n\n\n\n

Yes, there are non-rigorous approaches to math, which continue to be widely used in physics and engineering and other fields, as they always have been.  But none of these approaches have displaced proof as the gold standard whenever it\u2019s available.  If I had to speculate about why, I\u2019d say: if you use non-rigorous approaches, then even if it\u2019s clear to you under what conditions your results can be trusted, it\u2019s probably much less clear to others.  Also, even if only one segment of a research community cares about rigor, whatever earlier work that segment builds on will need to be rigorous as well \u2014 thereby exerting constant pressure in that direction.  Thus, the more collaborative a given research area becomes, the more important is rigor.<\/p>\n\n\n\n

For my money, the elucidation of the foundations of mathematics a century ago, by Cantor, Frege, Peano, Hilbert, Russell, Zermelo, G\u00f6del, Turing, and others, still stands as one of the greatest triumphs of human thought, up there with evolution or quantum mechanics or anything else.  It\u2019s true that the ideal set by these luminaries remains mostly aspirational.  When mathematicians say that a theorem has been \u201cproved,\u201d they still mean, as they always have, something more like: \u201cwe\u2019ve reached a social consensus that all the ideas are now in place for a strictly formal proof that could be verified by a machine … with the only task remaining being massive rote coding work that none of us has any intention of ever doing!\u201d  It\u2019s also true that mathematicians, being human, are subject to the full panoply of foibles you might expect: claiming to have proved things they haven\u2019t, squabbling over who proved what, accusing others of lack of rigor while hypocritically taking liberties themselves.  But just like love and honesty remain fine ideals no matter how often they\u2019re flouted, so too does mathematical rigor.<\/p>\n\n\n\n

Update:<\/font><\/strong> Here’s Horgan’s new post<\/a> (entitled “Okay, Maybe Proofs Aren’t Dying After All”), which also includes a contribution from Peter Woit.
<\/p>\n","protected":false},"excerpt":{"rendered":"

In 1993, the science writer John Horgan—who’s best known for his book The End of Science, and (of course) for interviewing me in 2016—wrote a now-(in)famous cover article for Scientific American entitled “The Death of Proof.” Mashing together a large number of (what I’d consider) basically separate trends and ideas, Horgan argued that math was […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"advanced_seo_description":"","jetpack_seo_html_title":"","jetpack_seo_noindex":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"_wpas_customize_per_network":false},"categories":[11],"tags":[],"class_list":["post-4133","post","type-post","status-publish","format-standard","hentry","category-nerd-interest"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/4133","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=4133"}],"version-history":[{"count":5,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/4133\/revisions"}],"predecessor-version":[{"id":4142,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=\/wp\/v2\/posts\/4133\/revisions\/4142"}],"wp:attachment":[{"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=4133"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=4133"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/scottaaronson.blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=4133"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}