> "Beware of bugs in the above code; I have only proved it correct, not tried it."
>
> [Donald Knuth](https://www-cs-faculty.stanford.edu/~knuth/faq.html)

> "When you have eliminated the impossible, whatever remains is often more improbable than your having made a mistake in one of your impossibility proofs."
>
> [Steven Kaas](http://lesswrong.com/lw/3m/rationalist_fiction/2p6#body_t1_2p6)

In some respects, there is nothing to be said; in other respects, there is much to be said. ["Probing the Improbable: Methodological Challenges for Risks with Low Probabilities and High Stakes"](https://arxiv.org/abs/0810.5515) discusses a basic issue with [existential threats](!Wikipedia): any useful discussion will be rigorous, hopefully with physics and math proofs; but proofs themselves are empirically unreliable.
Given that mathematical proofs have long been claimed to be the most reliable form of epistemology humans know and the only way to guarantee truth^[As a pragmatist & empiricist, I must have the temerity to disagree with the likes of Plato about the role of proof: if mathematical proof truly *was* so reliable, then I would have little to write about in this essay. However rigorous logic is, it is still created & used by fallible humans. There is no 'Platonia' we can tap into to obtain transcendent truth.], this sets a basic upper bound on how much confidence we can put on *any* belief, and given the lurking existence of systematic biases, it may even be possible for there to be too much evidence for a claim ([Gunn et al 2016](https://arxiv.org/abs/1601.00900 "Too good to be true: when overwhelming evidence fails to convince")).
There are other rare risks, from mental diseases[^mind] to hardware errors[^Hales-3] to how to deal with contradictions[^Wittgenstein], but we'll look at mathematical error.
[^Hales-3]: ["Mathematics in the Age of the Turing Machine"](https://arxiv.org/abs/1302.2898), Hales 2014:
> As an example, we will calculate the expected number of soft errors in one of the mathematical calculations of Section 1.17. The Atlas Project calculation of the E~8~ character table was a 77 hour calculation that required 64 gigabytes RAM [Ada07]. Soft errors rates are generally measured in units of failures-in-time (FIT). One FIT is defined as one error per 10^9^ hours of operation. If we assume a soft error rate of 10^3^ FIT per Mbit, (which is a typical rate for a modern memory device operating at sea level 15 [Tez04]), then we would expect there to be about 40 soft errors in memory during the calculation:
>
> $\frac{10^3 \text{FIT}}{\text{1Mbit}} \cdot \text{64GB} \cdot \text{77 hours} = \frac{10^3 \text{errors}}{10^9 \text{hours Mbit}} \cdot (64 \cdot 8 \cdot 10^3 \text{Mbit}) \cdot \text{77 hours} ≈ \text{39.4 errors}$
>
> This example shows that soft errors can be a realistic concern in mathematical calculations. (As added confirmation, the E~8~ calculation has now been repeated about 5 times with identical results.)...The soft error rate is remarkably sensitive to elevation; a calculation in Denver produces about three times more soft errors than the same calculation on identical hardware in Boston...Soft errors are depressing news in the ultra-reliable world of proof assistants. Alpha particles rain on perfect and imperfect software alike. In fact, because the number of soft errors is proportional to the execution time of a calculation, by being slow and methodical, the probability of a soft error during a calculation inside a proof assistant can be much higher than the probability when done outside.
# Error distribution
> "When I asked what it was, he said, 'It is the probability that the test bomb will ignite the whole atmosphere.' I decided I would check it myself! The next day when he came for the answers I remarked to him, 'The arithmetic was apparently correct but I do not know about the formulas for the capture cross sections for oxygen and nitrogen---after all, there could be no experiments at the needed energy levels.' He replied, like a physicist talking to a mathematician, that he wanted me to check the arithmetic not the physics, and left. I said to myself, 'What have you done, Hamming, you are involved in risking all of life that is known in the Universe, and you do not know much of an essential part?' I was pacing up and down the corridor when a friend asked me what was bothering me. I told him. His reply was, 'Never mind, Hamming, no one will ever blame you.'"
>
> [Richard Hamming](!Wikipedia) [1998](/docs/xrisks/1998-hamming.pdf "'Mathematics on a Distant Planet', Hamming 1998")

> "...of the two major thermonuclear calculations made that summer at Berkeley, they got one right and [one wrong](!Wikipedia "Castle Bravo#High yield")."
>
> [Toby Ord](!Wikipedia), [_The Precipice_](!Wikipedia "The Precipice: Existential Risk and the Future of Humanity") 2020

This upper bound on our certainty may force us to disregard certain rare risks because the effect of error on our estimates of existential risks is *asymmetric*: an error will usually reduce the risk, not increase it. The errors are not distributed in any kind of symmetrical around a mean: an existential risk is, by definition, bumping up against the upper bound on possible damage. If we were trying to estimate, say, average human height, and errors were distributed like a bell curve, then we could ignore them. But if we are calculating the risk of a super-asteroid impact which will kill all of humanity, an error which means the super-asteroid will actually kill humanity twice over is irrelevant because it's the same thing (we can't die twice); however, the mirror error---the super-asteroid actually killing half of humanity---matters a great deal!
![_XKCD_ [#809 "Los Alamos"](https://xkcd.com/809/)](/images/ai/2010-10-22-xkcd-809-losalamos.png "This comic refers to the Manhattan Project at Los Alamos, New Mexico, where in 1945 their development of the first nuclear weapon had progressed to the point that they were going to explode 'The Gadget' at Trinity Site. There was genuine concern that some unexpected result was possible, including the scenario about the atmosphere igniting. The scientists were almost certain that it would either work as expected, or just be a dud, but were unable to rule out several other scenarios. The test proceeded, and it worked as expected.")
[^mind]: There are various delusions (eg. [Cotard delusion](!Wikipedia)), [false memory syndrome](!Wikipedia)s, compulsive lying ([pseudologia fantastica](!Wikipedia)), disorders provoking [confabulation](!Wikipedia "Confabulation") such as the general symptom of [anosognosia](!Wikipedia); in a dramatic example of how the mind is what the brain does, some anosognosia can be temporarily cured by squirting cold water in an ear; from ["The Apologist and the Revolutionary"](http://lesswrong.com/lw/20/the_apologist_and_the_revolutionary/):
> Take the example of the woman discussed in Lishman's [_Organic Psychiatry_](http://www.amazon.com/Organic-Psychiatry-Psychological-Consequences-Cerebral/dp/0865428204/). After a right-hemisphere stroke, she lost movement in her left arm but continuously denied it. When the doctor asked her to move her arm, and she observed it not moving, she claimed that it wasn't actually her arm, it was her daughter's. Why was her daughter's arm attached to her shoulder? The patient claimed her daughter had been there in the bed with her all week. Why was her wedding ring on her daughter's hand? The patient said her daughter had borrowed it. Where was the patient's arm? The patient "turned her head and searched in a bemused way over her left shoulder"...In any case, a patient who has been denying paralysis for weeks or months will, upon having cold water placed in the ear, admit to paralysis, admit to having been paralyzed the past few weeks or months, and express bewilderment at having ever denied such an obvious fact. And then the effect wears off, and the patient not only denies the paralysis but denies ever having admitted to it.
[^Wittgenstein]: Most/all math results require their system to be consistent; but this is one particular philosophical view. [Ludwig Wittgenstein](!Wikipedia), in _[Remarks on the Foundations of Mathematics](!Wikipedia)_:
> If a contradiction were now actually found in arithmetic---that would only prove that an arithmetic with *such* a contradiction in it could render very good service; and it would be better for us to modify our concept of the certainty required, than to say it would really not yet have been a proper arithmetic.
[Saul Kripke](!Wikipedia), [reconstructing a Wittgensteinian skeptical argument](!Wikipedia "Wittgenstein on Rules and Private Language"), points out one way to react to such issues:
> A *skeptical* solution of a philosophical problem begins... by conceding that the skeptic's negative assertions are unanswerable. Nevertheless our ordinary practice or belief is justified because-contrary appearances notwithstanding-it need not require the justification the sceptic has shown to be untenable. And much of the value of the sceptical argument consists precisely in the fact that he has shown that an ordinary practice, if it is to be defended at all, cannot be defended in a certain way.
How big is this upper bound? Mathematicians have *often* made errors in proofs. But [it's](http://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-wrong) [rarer](!Wikipedia "List of disproved mathematical ideas") for ideas to be accepted for a long time and then rejected. But we can divide errors into 2 basic cases corresponding to [type I and type II errors](!Wikipedia):
1. Mistakes where the theorem is still true, but the proof was incorrect (type I)
2. Mistakes where the theorem was *false*, and the proof was also necessarily incorrect (type II)
Before someone comes up with a final answer, a mathematician may have [many levels of intuition](http://www.maa.org/sites/default/files/images/images/upload_library/22/Polya/07468342.di020715.02p0066x.pdf "'What Do I Know? A Study of Mathematical Self-Awareness', Davis 1983") in formulating & working on the problem, but we'll consider the final end-product where the mathematician feels satisfied that he has solved it.
Case 1 is perhaps the most common case, with innumerable examples; this is sometimes due to mistakes in the proof that anyone would accept is a mistake, but many of these cases are due to changing standards of proof.
For example, when David Hilbert discovered errors in Euclid's proofs which no one noticed before, the theorems were still true, and the gaps more due to Hilbert being a modern mathematician thinking in terms of formal systems (which of course Euclid did not think in).
(David Hilbert himself turns out to be a useful example of the other kind of error: his famous [list of 23 problems](!Wikipedia "Hilbert's problems") was accompanied by definite opinions on the outcome of each problem and sometimes timings, several of which were wrong or questionable[^Hilbert].)
Similarly, early calculus used 'infinitesimals' which were sometimes treated as being 0 and sometimes treated as an indefinitely small non-zero number; this was incoherent and strictly speaking, practically *all* of the calculus results were wrong because they relied on an incoherent concept---but of course the results were some of the greatest mathematical work ever conducted[^Neumann] and when later mathematicians put calculus on a more rigorous footing, they immediately re-derived those results (sometimes with important qualifications), and doubtless as modern math evolves other fields have sometimes needed to go back and clean up the foundations and will in the future.[^Mathematica]
Other cases are more straightforward, with mathematicians publishing multiple proofs/patches[^Nathanson] or covertly correcting papers[^Hales-1].
Sometimes they make it into textbooks: [Carmichael](!Wikipedia "Robert Daniel Carmichael") realized that his proof for [Carmichael's totient function conjecture](!Wikipedia), which is still open, was wrong only after [2 readers saw it in his 1914 textbook _The Theory of Numbers_ and questioned it](https://www.ams.org/journals/bull/1922-28-03/S0002-9904-1922-03504-5/S0002-9904-1922-03504-5.pdf "'Note on Euler's φ-Function', Carmichael 1922").
Attempts to formalize results into experimentally-verifiable results (in the case of physics-related math) or machine-checked proofs, or at least some sort of software form, sometimes turns up issues with[^Colton1] accepted[^Colton2] results[^Hales-2], although not always important (eg the correction in [Romero & Rubio 2013](http://www.unirioja.es/cu/anromero/MofC12.pdf "Homotopy groups of suspended classifying spaces: An experimental approach")).
Poincaré points out this mathematical version of the [pessimistic induction](!Wikipedia) in ["Intuition and Logic in Mathematics"](http://www-history.mcs.st-andrews.ac.uk/Extras/Poincare_Intuition.html "Henri Poincaré published _Intuition and Logic in mathematics_ as part of _La valeur de la science_ in 1905. It was translated into English by G B Halsted and published in 1907 as part of Poincaré's _The Value of Science_. A version of Poincaré's article is below."):
> Strange! If we read over the works of the ancients we are tempted to class them all among the intuitionalists. And yet nature is always the same; it is hardly probable that it has begun in this century to create minds devoted to logic. If we could put ourselves into the flow of ideas which reigned in their time, we should recognize that many of the old geometers were in tendency analysts. Euclid, for example, erected a scientific structure wherein his contemporaries could find no fault. In this vast construction, of which each piece however is due to intuition, we may still today, without much effort, recognize the work of a logician.
>
> ... What is the cause of this evolution? It is not hard to find. Intuition can not give us rigour, nor even certainty; this has been recognized more and more. Let us cite some examples. We know there exist continuous functions lacking derivatives. Nothing is more shocking to intuition than this proposition which is imposed upon us by logic. Our fathers would not have failed to say: "It is evident that every continuous function has a derivative, since every curve has a tangent." How can intuition deceive us on this point?
>
> ... I shall take as second example [Dirichlet's principle](!Wikipedia) on which rest so many theorems of mathematical physics; today we establish it by reasonings very rigorous but very long; heretofore, on the contrary, we were content with a very summary proof. A certain integral depending on an arbitrary function can never vanish. Hence it is concluded that it must have a minimum. The flaw in this reasoning strikes us immediately, since we use the abstract term function and are familiar with all the singularities functions can present when the word is understood in the most general sense. But it would not be the same had we used concrete images, had we, for example, considered this function as an electric potential; it would have been thought legitimate to affirm that electrostatic equilibrium can be attained. Yet perhaps a physical comparison would have awakened some vague distrust. But if care had been taken to translate the reasoning into the language of geometry, intermediate between that of analysis and that of physics, doubtless this distrust would not have been produced, and perhaps one might thus, even today, still deceive many readers not forewarned.
>
> ...A first question presents itself. Is this evolution ended? Have we finally attained absolute rigour? At each stage of the evolution our fathers also thought they had reached it. If they deceived themselves, do we not likewise cheat ourselves?
>
> We believe that in our reasonings we no longer appeal to intuition; the philosophers will tell us this is an illusion. Pure logic could never lead us to anything but tautologies; it could create nothing new; not from it alone can any science issue. In one sense these philosophers are right; to make arithmetic, as to make geometry, or to make any science, something else than pure logic is necessary.
[^Mathematica]: Stephen Wolfram mentions a recent example I hadn't run into used before, [in a long discussion of expanding Mathematica to automatically incorporate old papers' results](http://blog.stephenwolfram.com/2014/08/computational-knowledge-and-the-future-of-pure-mathematics/ "Computational Knowledge and the Future of Pure Mathematics")
> Of course, there are all sorts of practical issues. Newer papers are predominantly in T
> "Lefschetz was a purely intuitive mathematician. It was said of him that he had never given a completely correct proof, but had never made a wrong guess either."
>
> Gian-Carlo Rota^[["Fine Hall in its golden age: Remembrances of Princeton in the early fifties"](https://web.archive.org/web/20170419194138/https://www.princeton.edu/mudd/finding_aids/mathoral/pmcxrota.htm), _Indiscrete Thoughts_]

Case 2 is disturbing, since it is a case in which we wind up with false beliefs and also false beliefs about our beliefs (we no longer know that we don't know). Case 2 could lead to extinction.
The prevalence of case 1 might lead us to be very pessimistic; case 1, case 2, what's the difference? We have demonstrated a large error rate in mathematics (and physics is probably even worse off). Except, errors do not seem to be evenly & randomly distributed between case 1 and case 2. There seem to be far more case 1s than case 2s, as already mentioned in the early calculus example: far more than 50% of the early calculus results were correct when checked more rigorously. [Richard Hamming (1998)](/docs/xrisks/1998-hamming.pdf "'Mathematics on a Distant Planet', Hamming 1998") attributes to [Ralph Boas](!Wikipedia "Ralph P. Boas, Jr.") a comment that while editing _[Mathematical Reviews](!Wikipedia)_ that "of the new results in the papers reviewed most are true but the corresponding proofs are perhaps half the time plain wrong". (WP mentions as well that "His first mathematics publication was written...after he discovered an incorrect proof in another paper.") [Gian-Carlo Rota](!Wikipedia) gives us an example with Hilbert:
> Once more let me begin with Hilbert. When the Germans were planning to publish Hilbert's collected papers and to present him with a set on the occasion of one of his later birthdays, they realized that they could not publish the papers in their original versions because they were full of errors, some of them quite serious. Thereupon they hired a young unemployed mathematician, [Olga Taussky-Todd](!Wikipedia), to go over Hilbert's papers and correct all mistakes. Olga labored for three years; it turned out that all mistakes could be corrected without any major changes in the statement of the theorems. There was one exception, a paper Hilbert wrote in his old age, which could not be fixed; it was a purported proof of the continuum hypothesis, you will find it in a volume of the _Mathematische Annalen_ of the early thirties. At last, on Hilbert's birthday, a freshly printed set of Hilbert's collected papers was presented to the Geheimrat. Hilbert leafed through them carefully and did not notice anything.^[["Ten Lessons I wish I had been Taught"](http://alumni.media.mit.edu/~cahn/life/gian-carlo-rota-10-lessons.html#mistakes), Gian-Carlo Rota 1996]
So only one of those papers was irreparable, while all the others were correct and fixable? Rota himself experienced this:
> Now let us shift to the other end of the spectrum, and allow me to relate another personal anecdote. In the summer of 1979, while attending a philosophy meeting in Pittsburgh, I was struck with a case of detached retinas. Thanks to Joni's prompt intervention, I managed to be operated on in the nick of time and my eyesight was saved. On the morning after the operation, while I was lying on a hospital bed with my eyes bandaged, Joni dropped in to visit. Since I was to remain in that Pittsburgh hospital for at least a week, we decided to write a paper. Joni fished a manuscript out of my suitcase, and I mentioned to her that the text had a few mistakes which she could help me fix. There followed twenty minutes of silence while she went through the draft. "*Why, it is all wrong!*" she finally remarked in her youthful voice. She was right. Every statement in the manuscript had something wrong. Nevertheless, after laboring for a while, she managed to correct every mistake, and the paper was eventually published.
>
> There are two kinds of mistakes. There are fatal mistakes that destroy a theory; but there are also contingent ones, which are useful in testing the stability of a theory.
A mathematician of my acquaintance referred me to [pg118](http://web.archive.org/web/20121031161104/http://www.maths.gla.ac.uk/~tl/images/Jech_p118.png) of [_The Axiom of Choice_](/docs/math/1973-jech-theaxiomofchoice.pdf), Jech 1973; he had found the sustained effect of the 5 footnotes humorous:
> 1. The result of Problem 11 contradicts the results announced by Levy [1963b]. Unfortunately, the construction presented there cannot be completed.
> 2. The transfer to ZF was also claimed by Marek [1966] but the outlined method appears to be unsatisfactory and has not been published.
> 3. A contradicting result was announced and later withdrawn by Truss [1970].
> 4. The example in Problem 22 is a counterexample to another condition of Mostowski, who conjectured its sufficiency and singled out this example as a test case.
> 5. The independence result contradicts the claim of Felgner [1969] that the Cofinality Principle implies the Axiom of Choice. An error has been found by Morris (see Felgner's corrections to [1969]).
And referred me also to the entries in the index of _Fourier Analysis_ by Tom Körner concerning the problem of the ["pointwise convergence of Fourier series"](http://golem.ph.utexas.edu/category/2013/01/carlesons_theorem.html "'Carleson's Theorem', Tom Leinster"):
> - excessive optimism
>
> - [Cauchy](!Wikipedia "Augustin-Louis Cauchy"), 3
> - [Dedekind](!Wikipedia "Richard Dedekind"), [Dirichlet](!Wikipedia "Johann Peter Gustav Lejeune Dirichlet") and [Weierstrass](!Wikipedia "Karl Weierstrass"), 67
> - Dirichlet, [Gauss](!Wikipedia "Carl Friedrich Gauss"), [Green](!Wikipedia "George Green (mathematician)"), [Kelvin](!Wikipedia "William Thomson, 1st Baron Kelvin") and [Riemann](!Wikipedia "Bernhard Riemann"), 126
> - [Faraday](!Wikipedia "Michael Faraday") and Morse^[There are 2 20^th^ century mathematicians, born too late to work with Faraday, and the telegraph inventor Samuel Morse who while overlapping with Faraday, has a Wikipedia entry mentioning no work in mathematics; I do not know which Morse may be meant.], 333
> - [Galois](!Wikipedia "Evariste Galois"), 38
> - Hegel, 370
> - [Hermite](!Wikipedia "Charles Hermite") and [Poincaré](!Wikipedia "Henri Poincare"). 42
> - [Pearson](!Wikipedia "Karl Pearson"), 424
> - [Poisson](!Wikipedia "Simeon Denis Poisson"), 119
> - [Steiner](!Wikipedia "Jakob Steiner"), 163
> - excessive pessimism
>
> - [Delambre](!Wikipedia "Jean Baptiste Joseph Delambre"), 473--4
> - general, 4, 74
> - [Lagrange](!Wikipedia "Joseph Louis Lagrange"), 473
> - [Tchebychev](!Wikipedia "Pafnuty Chebyshev"), 198
Some problems are notorious for provoking repeated false proofs. [P=NP](!Wikipedia) attracts countless cranks and [serious attempts](http://www.win.tue.nl/~gwoegi/P-versus-NP.htm "This page collects links around papers that try to settle the 'P versus NP' question (in either way)."), of course, but also amusing is [apparently the Jacobian Conjecture](http://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-wrong/36020#36020):
> The (in)famous Jacobian Conjecture was considered a theorem since a 1939 publication by Keller (who claimed to prove it). Then Shafarevich found a new proof and published it in some conference proceedings paper (in early 1950-ies). This conjecture states that any polynomial map from C^2 to C^2 is invertible if its Jacobian is nowhere zero. In 1960-ies, Vitushkin found a counterexample to all the proofs known to date, by constructing a complex analytic map, not invertible and with nowhere vanishing Jacobian. It is still a main source of embarrassment for Arxiv.org contributors, who publish about 3--5 false proofs yearly. Here is a funny refutation for one of the proofs: ["Comment on a Paper by Yucai Su On Jacobian Conjecture (Dec 30, 2005)"](https://arxiv.org/abs/math/0604049 "Moh 2006")
>
>> The problem of Jacobian Conjecture is very hard. Perhaps it will take human being another 100 years to solve it. Your attempt is noble, Maybe the Gods of Olympus will smile on you one day. Do not be too disappointed. B. Sagre has the honor of publishing three wrong proofs and C. Chevalley mistakes a wrong proof for a correct one in the 1950's in his Math Review comments, and I.R. Shafarevich uses Jacobian Conjecture (to him it is a theorem) as a fact...
This look into the proverbial sausage factory should not come as a surprise to anyone taking an [Outside View](http://wiki.lesswrong.com/wiki/Outside_view): why wouldn't we expect any area of intellectual endeavour to have error rates within a few orders of magnitude as any other area? How absurd to think that the rate might be ~0%; but it's also a little questionable to be as optimistic as [Anders Sandberg's mathematician friend](http://www.aleph.se/andart/archives/2012/09/flaws_in_the_perfection.html "Flaws in the Perfection"): "he responded that he thought a far smaller number [1%] of papers in math were this flawed."
# Heuristics
Other times, the correct result is known and proven, but many are unaware of the answers[^enduring]. The famous [Millennium Problems](!Wikipedia)---those that have been solved, anyway---have a long history of failed proofs (Fermat surely did not prove [Fermat's Last Theorem](!Wikipedia) & may have realized this only after boasting[^Fermat-last-boast] and neither did [Lindemann](!Wikipedia "Ferdinand von Lindemann")[^mathworld]). What explains this? The guiding factor that keeps popping up when mathematicians make leaps seems to go under the name of 'elegance' or [mathematical beauty](!Wikipedia), which widely considered important[^Goldstein][^Erdos][^Sinclair1]. This imbalance suggests that mathematicians are quite correct when they say proofs are not the heart of mathematics and that they possess insight into math, a 6^th^ sense for mathematical truth, a nose for aesthetic beauty which correlates with veracity: they disproportionately go after theorems rather than their negations.
Why this is so, I do not know.
Outright Platonism like Godel apparently believed in seems unlikely---mathematical expertise resembles a complex skill like chess-playing more than it does a sensory modality like vision. Possibly they have well-developed heuristics and short-cuts and they focus on the subsets of results on which those heuristics work well (the drunk searching under the spotlight), or perhaps they *do* run full rigorous proofs but are doing so subconsciously and merely express themselves ineptly consciously with omissions and erroneous formulations 'left as an exercise for the reader'[^Sinclair2].
[^Sinclair1]: From ["Aesthetics as a Liberating Force in Mathematics Education?"](/docs/math/2009-sinclair.pdf), by Nathalie Sinclair (reprinted in [_The Best Writing on Mathematics 2010_](http://www.amazon.com/Best-Writing-Mathematics-2010/dp/0691148414/), ed. Mircea Pitici); pg208:
> There is a long tradition in mathematics of describing proofs and theorems in aesthetic terms, often using words such as 'elegance' and 'depth'. Further, mathematicians have also argued that their subject is more akin to an art than it is to a science (see [Hardy, 1967](!Wikipedia "A Mathematician's Apology"); Littlewood, 1986; Sullivan 1925/1956), and, like the arts, ascribe to mathematics aesthetic goals. For example, the mathematician W. Krull ([1930/1987](/docs/math/1987-krull.pdf "The aesthetic viewpoint in mathematics")) writes: "the primary goals of the mathematician are aesthetic, and not epistemological" (p. 49). This statement seems contradictory with the oft-cited concern of mathematics with finding or discovering truths, but it emphasises the fact that the mathematician's interest is in expressing truth, and in doing so in clever, simple, succinct ways.
>
> While Krull focuses on mathematical expression, the mathematician H. Poincare ([1908/1966](http://paradise.caltech.edu/ist4/lectures/Poincare_Reflections.pdf "Mathematical Creation")) concerns himself with the psychology of mathematical invention, but he too underlines the aesthetic dimension of mathematics, not the logical. In Poincare's theory, a large part of a mathematician's work is done at the subconscious level, where an aesthetic sensibility is responsible for alerting the mathematicians to the most fruitful and interesting of ideas. Other mathematicians have spoken of this special sensibility as well and also in terms of the way it guides mathematicians to choose certain problems. This choice is essential in mathematic given that there exists no external reality against which mathematicians can decide which problems or which branches of mathematics are important (see von Neumann, 1947 ["The Mathematician"]): the choice involves human values and preference---and, indeed, these change over time, as exemplified by the dismissal of geometry by some prominent mathematicians in the early 20^th^ century (see [Whiteley, 1999](http://www.math.yorku.ca/Who/Faculty/Whiteley/cmesg.pdf)).
>
> - Littlewood, 1986: "The mathematician's art of work"; in B. Bollobas (ed.), _Littlewood's miscellany_, Cambridge University press
> - Sullivan 1925/1956: "Mathematics as an art"; in J. Newman (ed.), _The world of mathematics_, vol 3 (p 2015--2021)
[^Sinclair2]: From pg 211--212, Sinclair 2009:
> The survey of mathematicians conducted by [Wells (1990)](/docs/math/1990-wells.pdf) provides a more empirically-based challenge to the intrinsic view of the mathematical aesthetic. Wells obtained responses from over 80 mathematicians, who were asked to identify the most beautiful theorem from a given set of 24 theorems. (These theorems were chosen because they were 'famous', in the sense that Wells judged them to be well-known by most mathematicians, and of interest to the discipline in general, rather than to a particular subfield.) Wells finds that the mathematicians varied widely in their judgments. More interestingly, in explaining their choices, the mathematicians revealed a wide range of personal responses affecting their aesthetic responses to the theorems. Wells effectively puts to rest the belief that mathematicians have some kind of secret agreement on what counts as beautiful in mathematics...Burton's (2004) work focuses on the practices of mathematicians and their understanding of those practices. Based on extensive interviews with a wide range of mathematicians...She points out that mathematicians range on a continuum from unimportant to crucial in terms of their positionings on the role of the aesthetic, with only 3 of the 43 mathematicians dismissing its importance. For example, one said "Beauty doesn't matter. I have never seen a beautiful mathematical paper in my life" (p. 65). Another mathematician was initially dismissive about mathematical beauty but later, when speaking about the review process, said: "If it was a very elegant way of doing things, I would be inclined to forgive a lot of faults" (p. 65).
>
> - Burton, Leone (2004): [_Mathematicians as enquirers: Learning about learning mathematics_](http://www.amazon.com/Mathematicians-Enquirers-Learning-Mathematics-Education/dp/1402078595/); Dordrecht: Kluwer Academic Publishers
[^Goldstein]: To take a random example (which could be multiplied indefinitely); from [Gödel and the Nature of Mathematical Truth: A Talk with Rebecca Goldstein](http://www.edge.org/3rd_culture/goldstein05/goldstein05_index.html) (6.8.2005):
> Einstein told the philosopher of science [Hans Reichenbach](!Wikipedia) that he'd known even before the solar eclipse of 1918 supported his general theory of relativity that the theory must be true because it was so beautiful. And [Hermann Weyl](!Wikipedia), who worked on both relativity theory and quantum mechanics, said "My work always tried to unite the true with the beautiful, but when I had to choose one or the other, I usually chose the beautiful."...Mathematics seems to be the one place where you don't have to choose, where truth and beauty are always united. One of my all-time favorite books is _[A Mathematician's Apology](!Wikipedia)_. [G.H. Hardy](!Wikipedia) tries to demonstrate to a general audience that mathematics is intimately about beauty. He gives as examples two proofs, one showing that the square root of 2 is irrational, the other showing that there's no largest prime number. Simple, easily graspable proofs, that stir the soul with wonder.
[^Erdos]: Nathanson 2009 claims the opposite:
> Many mathematicians have the opposite opinion; they do not or cannot distinguish the beauty or importance of a theorem from its proof. A theorem that is first published with a long and difficult proof is highly regarded. Someone who, preferably many years later, finds a short proof is "brilliant." But if the short proof had been obtained in the beginning, the theorem might have been disparaged as an "easy result." Erdős was a genius at finding brilliantly simple proofs of deep results, but, until recently, much of his work was ignored by the mathematical establishment.
[^enduring]: An example of this would be ["An Enduring Error"](http://digital.lib.washington.edu/dspace/bitstream/handle/1773/4592/An_enduring_error.pdf?sequence=1), Branko Grünbaum:
> Mathematical truths are immutable, but mathematicians do make errors, especially when carrying out non-trivial enumerations. Some of the errors are "innocent"---plain mistakes that get corrected as soon as an independent enumeration is carried out. For example, Daublebsky [14] in 1895 found that there are precisely 228 types of configurations (123), that is, collections of 12 lines and 12 points, each incident with three of the others. In fact, as found by Gropp [19] in 1990, the correct number is 229. Another example is provided by the enumeration of the uniform tilings of the 3-dimensional space by Andreini [1] in 1905; he claimed that there are precisely 25 types. However, as shown [20] in 1994, the correct number is 28. Andreini listed some tilings that should not have been included, and missed several others---but again, these are simple errors easily corrected...It is surprising how errors of this type escape detection for a long time, even though there is frequent mention of the results. One example is provided by the enumeration of 4-dimensional simple polytopes with 8 facets, by Brückner [7] in 1909. He replaces this enumeration by that of 3-dimensional "diagrams" that he interpreted as Schlegel diagrams of convex 4-polytopes, and claimed that the enumeration of these objects is equivalent to that of the polytopes. However, aside from several "innocent" mistakes in his enumeration, there is a fundamental error: While to all 4-polytopes correspond 3-dimensional diagrams, there is no reason to assume that every diagram arises from a polytope. At the time of Brückner's paper, even the corresponding fact about 3-polyhedra and 2-dimensional diagrams has not yet been established---this followed only from Steinitz's characterization of complexes that determine convex polyhedra [45], [46]. In fact, in the case considered by Brückner, the assumption is not only unjustified, but actually wrong: One of Brückner's polytopes does not exist, see [25].
>
> ...Polyhedra have been studied since antiquity. It is, therefore, rather surprising that even concerning some of the polyhedra known since that time there is a lot of confusion, regarding both terminology and essence. But even more unexpected is the fact that many expositions of this topic commit serious mathematical and logical errors. Moreover, this happened not once or twice, but many times over the centuries, and continues to this day in many printed and electronic publications; the most recent case is in the second issue for 2008 of this journal...With our understandings and exclusions, there are fourteen convex polyhedra that satisfy the local criterion and should be called "Archimedean", but only thirteen that satisfy the global criterion and are appropriately called "uniform" (or "semiregular"). Representatives of the thirteen uniform convex polyhedra are shown in the sources mentioned above, while the fourteenth polyhedron is illustrated in Figure 1. It satisfies the local criterion but not the global one, and therefore is---in our terminology---Archimedean but not uniform. The history of the realization that the local criterion leads to fourteen polyhedra will be discussed in the next section; it is remarkable that this development occurred only in the 20^th^ century. This implies that prior to the twentieth century all enumerations of the polyhedra satisfying the local criterion were mistaken. Unfortunately, many later enumerations make the same error.
[^mathworld]: From [MathWorld](!Wikipedia), ["Fermat's Last Theorem"](http://mathworld.wolfram.com/FermatsLastTheorem.html):
> Much additional progress was made over the next 150 years, but no completely general result had been obtained. Buoyed by false confidence after his proof that pi is transcendental, the mathematician Lindemann proceeded to publish several proofs of Fermat's Last Theorem, all of them invalid (Bell 1937, pp. 464--465). A prize of 100000 German marks, known as the Wolfskehl Prize, was also offered for the first valid proof (Ball and Coxeter 1987, p. 72; Barner 1997; Hoffman 1998, pp. 193--194 and 199).
>
> A recent false alarm for a general proof was raised by Y. Miyaoka (Cipra 1988) whose proof, however, turned out to be flawed. Other attempted proofs among both professional and amateur mathematicians are discussed by vos Savant (1993), although vos Savant erroneously claims that work on the problem by Wiles (discussed below) is invalid.
[^Fermat-last-boast]: Dana Mackinzie, [_The Universe in Zero Words: The Story of Mathematics as Told through Equations_](http://www.amazon.com/gp/product/B007BP3ATU/) (as quoted by [John D. Cook](http://www.johndcook.com/blog/2013/10/15/fermats-proof-of-his-last-theorem/)):
> Fermat repeatedly bragged about the _n_ = 3 and _n_ = 4 cases and posed them as challenges to other mathematicians ... But he never mentioned the general case, _n_ = 5 and higher, in any of his letters. Why such restraint? Most likely, [Weil](!Wikipedia "André Weil") argues, because Fermat had realized that his "truly wonderful proof" did not work in those cases...Every mathematician has had days like this. You think you have a great insight, but then you go out for a walk, or you come back to the problem the next day, and you realize that your great idea has a flaw. Sometimes you can go back and fix it. And sometimes you can't.
We could try to justify the heuristic paradigm by appealing to as-yet poorly understood aspects of the brain, like our visual cortex: argue that what is going on is that mathematicians are subconsciously doing tremendous amounts of computation (like we do tremendous amounts of computation in a thought as ordinary as recognizing a face), which they are unable to bring up explicitly.
So after prolonged introspection and some comparatively simple explicit symbol manipulation or thought, they *feel* that a conjecture is true and this is due to a summary of said massive computations.
Perhaps they are checking many instances? Perhaps they are [white-box testing](!Wikipedia) and looking for boundaries?
Could there be some sort of "logical probability" where going down possible proof-paths yield probabilistic information about the final target theorem, maybe in some sort of [Monte Carlo tree search](!Wikipedia "Monte Carlo method") of proof-trees?
Do [sleep](!Wikipedia "Sleep and memory") serve to consolidate & prune & [replay](!Wikipedia "Hippocampal replay") memories of incomplete lines of thought, finetuning heuristics or intuitions for future attacks and getting deeper into a problem (perhaps analogous to [expert iteration](https://arxiv.org/abs/1712.01815 "'Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm', Silver et al 2017"))?
Reading great mathematicians like [Terence Tao](!Wikipedia) discuss the heuristics they use on unsolved problems[^Tao], they bear some resemblances to computer science techniques.
This would be consistent with a preliminary observation about [how long it takes](https://arxiv.org/abs/1202.3936 "'On the distribution of time-to-proof of mathematical conjectures', Hisano & Sornette 2012") [to solve](/docs/math/2013-hisano.pdf "'Challenges to the Assessment of Time-to-Proof of Mathematical Conjectures', Hisano & Sornette 2013") [mathematical conjectures](https://aiimpacts.org/resolutions-of-mathematical-conjectures-over-time/ "Resolutions of mathematical conjectures over time"): while inference is rendered difficult by the exponential growth in the global population and of mathematicians, the distribution of time-to-solution roughly matches a memoryless [exponential distribution](!Wikipedia) (one with a constant chance of solving it in any time period) rather than a more intuitive distribution like a type 1 [survivorship curve](!Wikipedia) (where a conjecture gets easier to solve over time, perhaps as related mathematical knowledge accumulates), suggesting a model of mathematical activity in which many independent random attempts are made, each with a small chance of success, and eventually one succeeds.
This idea of extensive unconscious computation neatly accords with Poincaré's account of mathematical creativity in which after long fruitless effort (preparation), he abandoned the problem for a time and engaged in ordinary activities ([incubation](!Wikipedia "Incubation (psychology)")), is suddenly struck by an answer or insight, and then verifies its correctness consciously.
The existence of an incubation effect seems confirmed by psychological studies and particular the observation that incubation effects increase with the time allowed for incubation & also if the subject does not undertake demanding mental tasks during the incubation period (see [Sio & Ormerod 2009](http://www.psy.cmu.edu/~unsio/Sio_Ormerod_meta_analysis_incubation_PB.pdf "Does incubation enhance problem-solving? A meta-analytic review")), and is consistent with extensive unconscious computation.
Some of this computation may happen during sleep; sleep & cognition have long been associated in a murky fashion ("sleep on it"), but it may have to do with reviewing the events of the day & difficult tasks, with relevant [memories](!Wikipedia "Sleep and memory") reinforced or perhaps more thinking going on.
I've seen more than one suggestion of this, and mathematician [Richard K. Guy](!Wikipedia) suggests this as well.[^Guy]
(It's unclear how many results occur this way; [Stanislaw Ulam](!Wikipedia) mentions finding one result but never again[^Ulam-dream]; J Thomas mentions one success but one failure by a teacher[^Thomas]; R. W. Thomason dreamed of a dead friend making a clearly false claim and published material based on his disproof of the ghost's claim[^Thomason]; and [Leonard Eugene Dickson](!Wikipedia) reportedly had a useful dream & an early survey of 69 mathematicians yielded 63 nulls, 5 low-quality results, and 1 hit[^Hadamard].)
[^Thomason]: ["Higher algebraic K-theory of schemes and of derived categories"](/docs/math/1990-thomason.pdf), Thomason & Trobaugh 1990:
> The first author must state that his coauthor and close friend, Tom Trobaugh, quite intelligent, singularly original, and inordinately generous, killed himself consequent to endogenous depression. 94 days later, in my dream, Tom's simulacrum remarked, "The direct limit characterization of perfect complexes shows that they extend, just as one extends a coherent sheaf." Awaking with a start, I knew this idea had to be wrong, since some perfect complexes have a non-vanishing K~0~ obstruction to extension. I had worked on this problem for 3 years, and saw this approach to be hopeless. But Tom's simulacrum had been so insistent, I knew he wouldn't let me sleep undisturbed until I had worked out the argument and could point to the gap. This work quickly led to the key results of this paper. To Tom, I could have explained why he must be listed as a coauthor.
[^Ulam-dream]: January 14, 1974, in "Conversations with Gian-Carlo Rota"; as quoted on pg262 of [_Turing's Cathedral_](http://www.amazon.com/Turings-Cathedral-Origins-Digital-Universe/dp/1400075998/) (2012) by [George Dyson](!Wikipedia "George Dyson (science historian)"):
> Once in my life I had a mathematical dream which proved correct. I was twenty years old. I thought, my God, this is wonderful, I won't have to work, it will all come in dreams! But it never happened again.
[^Hadamard]: [Jacques Hadamard](!Wikipedia), [_An Essay on the Psychology of Invention in the Mathematical Field_](https://archive.org/details/eassayonthepsych006281mbp) (1945), pg27
> Let us come to mathematicians. One of them, Maillet, started a first inquiry as to their methods of work. One famous question, in particular, was already raised by him that of the "mathematical dream", it having been suggested often that the solution of problems that have defied investigation may appear in dreams. Though not asserting the absolute non-existence of "mathematical dreams", Maillet's inquiry shows that they cannot be considered as having a serious significance. Only one remarkable observation is reported by the prominent American mathematician, Leonard Eugene Dickson, who can positively assert its accuracy...Except for that very curious case, most of the 69 correspondents who answered Maillet on that question never experienced any mathematical dream (I never did) or, in that line, dreamed of wholly absurd things, or were unable to state precisely the question they happened to dream of. 5 dreamed of quite naive arguments. There is one more positive answer; but it is difficult to take account of it, as its author remains anonymous.
[^Thomas]: [J Thomas](http://crookedtimber.org/2014/11/06/philosopher-dreams-of-saving-electric-cats/#comment-581763):
> Once after I had spent several days trying to prove a topology theorem, I dreamed about it and woke up with as counterexample. In the dream it just constructed itself, and I could see it. I didn't have a fever then, though. Later one of my teachers, an old Polish woman, explained her experience. She kept a notebook by her bed so she could write down any insights she got in her sleep. She woke up in the night with a wonderful proof, and wrote it down, and in the morning when she looked at it it was all garbage. "You cannot do math in your sleep. You will have to work."
[^Guy]: pg190--191 of [_Fascinating Mathematical People_](http://www.amazon.com/Fascinating-Mathematical-People-Interviews-Memoirs/dp/0691148295), edited by Albers 2011:
> **Guy**: If I do any mathematics at all I think I do it in my sleep.
>
> **MP**: Do you think a lot of mathematicians work that way?
>
> **Guy**: I do. Yes. The human brain is a remarkable thing, and we are a long way from understanding how it works. For most mathematical problems, immediate thought and pencil and paper---the usual things one associates with solving mathematical problems---are just totally inadequate. You need to understand the problem, make a few symbols on paper and look at them. Most of us, as opposed to Erdős who would probably give an answer to a problem almost immediately, would then probably have to go off to bed, and, if we're lucky, when we wake up in the morning, we would already have some insight into the problem. On those rare occasions when I have such insight, I quite often don't know that I have it, but when I come to work on the problem again, to put pencil to paper, somehow the ideas just seem to click together, and the thing goes through. It is clear to me that my brain must have gone on, in an almost combinatorial way, checking the cases or doing an enormous number of fairly trivial arithmetical computations. It seems to know the way to go. I first noticed this with [chess endgames](!Wikipedia), which are indeed finite combinatorial problems. The first indication that I was interested in combinatorics---I didn't know I had the interest, and I didn't even know there was such a subject as combinatorics---was that I used to compose chess endgames. I would sit up late into the night trying to analyze a position. Eventually I would sink into slumber and wake up in the morning to realize that if I had only moved the pawns over one file the whole thing would have gone through clearly. My brain must have been checking over this finite but moderately large number of possibilities during the night. I think a lot of mathematicians must work that way.
>
> **MP**: Have you talked to any other mathematicians about that?
>
> **Guy**: No. But in Jacques Hadamard's book on invention in the mathematical field, he quotes some examples there where it is fairly clear that people do that kind of thing. There was someone earlier this week who was talking about Jean-Paul Serre. He said that if you ask Serre a question he either gives you the answer immediately, or, if he hesitates, and you push him in any way, he will say, "How can I think about the question when I don't know the answer?" I thought that was a lovely remark. At a much lower level, one should think, "What shape should the answer be?" Then your mind can start checking whether you're right and how to find some logical sequence to get you where you want to go.
[^Tao]: Tao left a [lengthy comment](http://rjlipton.wordpress.com/2010/06/19/guessing-the-truth/#comment-3711) on a previously linked Lipton post:
> It is possible to gather reasonably convincing support for a conjecture by a variety of means, long before it is actually proven, though many mathematicians are reluctant to argue too strongly based on such support due to the lack of rigour or the risk of embarrassment in hindsight. Examples of support include:
>
> - Numerical evidence; but one has to be careful in situations where the null hypothesis would also give comparable numerical evidence. The first ten trillion zeroes of zeta on the critical line is, in my opinion, only mild evidence in favour of RH (the null hypothesis may be, for instance, that the zeroes go haywire once log log t becomes sufficiently large); but the numerical data on spacings of zeroes is quite convincing evidence for the GUE hypothesis, in my view. (It is a priori conceivable that the spacings are distributed according to GUE plus another correction that dominates when log log t (say) is large, but this begins to strain Occam's razor.)
> - Non-trivial special cases. But it depends on how "representative" one believes the special cases to be. For instance, if one can verify low-dimensional cases of a conjecture that is true in high dimensions, this is usually only weak (but not entirely insignificant) evidence, as it is possible that there exist high-dimensional pathologies that sink the conjecture but cannot be folded up into a low-dimensional situation. But if one can do all odd-dimensional cases, and all even-dimensional cases up to dimension 8 (say), then that begins to look more convincing.
> - Proofs of parallel, analogous, or similar conjectures. Particularly if these proofs were non-trivial and led to new insights and techniques. RH in function fields is a good example here; it raises the hope of some sort of grand unified approach to GRH that somehow handles all number fields (or some other general class) simultaneously.
> - Converse of the conjecture is provable, and looks "optimal" somehow. One might be able to construct a list of all obvious examples of objects with property X, find significant difficulty extending the list, and then conjecture that this is list is complete. This is a common way to make conjectures, but can be dangerous, as one may simply have a lack of imagination. So this is thin evidence by itself (many false conjectures have arisen from this converse-taking method), but it does carry a little bit of weight once combined with other strands of evidence.
> - Conjecture is ambitious and powerful, and yet is not immediately sunk by the obvious consistency checks. This is vaguely analogous to the concept of a "falsifiable theory" in science. A strong conjecture could have many powerful consequences in a variety of disparate areas of mathematics---so powerful, in fact, that one would not be surprised that they could be disproven with various counterexamples. But surprisingly, when one checks the cases that one does understand quite well, the conjecture holds up. A typical example here might include a very general conjectured identity which, when specialised to various well-understood special cases, become a provable identity---but with the identity in each special case being provable by very different methods, and the connection between all the identities being mysterious other than via the conjecture. The general conjecture that the primes behave pseudorandomly after accounting for small moduli is an example of such a conjecture; we usually can't control how the primes behave, but when we can, the pseudorandomess heuristic lines up perfectly.
> - Attempts at disproof run into interesting obstacles. This one is a bit hard to formalise, but sometimes you can get a sense that attempts to disprove a conjecture are failing not due to one's own lack of ability, or due to accidental contingencies, but rather due to "enemy activity"; some lurking hidden structure to the problem, corners of which emerge every time one tries to build a counterexample. The question is then whether this "enemy" is stupid enough to be outwitted by a sufficiently clever counterexample, or is powerful enough to block all such attempts. Identifying this enemy precisely is usually the key to resolving the conjecture (or transforming the conjecture into a stronger and better conjecture).
> - Conjecture generalises to a broader conjecture that enjoys support of the types listed above. The twin prime conjecture, by itself, is difficult to support on its own; but when it comes with an asymptotic that one can then verify numerically to high accuracy and is a consequence of the much more powerful prime tuples conjecture (and more generally, the pseudorandomness heuristic for the primes) which is supported both because of its high falsifiability and also its nature as an optimal-looking converse (the only structure to the primes are the "obvious" structures), it becomes much more convincing. Another textbook example is the Poincare conjecture, which became much more convincing after being interpreted as a special case of geometrisation (which had a lot of support, e.g. the two-dimensional analogue, Haken manifolds, lots of falsifiable predictions, etc.).
>
> It can be fun (though a little risky, reputation-wise) to debate how strong various pieces of evidence really are, but one soon reaches a point of diminishing returns, as often we are limited by our own ignorance, lack of imagination, or cognitive biases. But we are at least reasonably able to perform *relative* comparisons of the strength of evidence of two conjectures in the same topic (I guess complexity theory is full of instances of this...).
Heuristics, however, do not generalize, and fail outside their particular domain. Are we fortunate enough that the domain mathematicians work in is---deliberately or accidentally---just that domain in which their heuristics/intuition succeeds? [Sandberg](http://www.aleph.se/andart/archives/2012/09/flaws_in_the_perfection.html) suggests not:
> Unfortunately I suspect that the connoisseurship of mathematicians for truth might be local to their domain. I have discussed with friends about how "brittle" different mathematical domains are, and our consensus is that there are definitely differences between logic, geometry and calculus. Philosophers also seem to have a good nose for what works or doesn't in their domain, but it doesn't seem to carry over to other domains. Now moving outside to applied domains things get even trickier. There doesn't seem to be the same "nose for truth" in risk assessment, perhaps because it is an interdisciplinary, messy domain. The cognitive abilities that help detect correct decisions are likely local to particular domains, trained through experience and maybe talent (i.e. some conformity between neural pathways and deep properties of the domain). The only thing that remains is general-purpose intelligence, and that has its own limitations.
[Leslie Lamport](!Wikipedia) advocates for machine-checked proofs and a more rigorous style of proofs similar to [natural deduction](!Wikipedia), noting a mathematician acquaintance guesses at a broad error rate of 1⁄3[^Lamport-third] and that he routinely found mistakes in his own proofs and, worse, believed false conjectures[^Lamport-mistakes].
[^Lamport-third]: From his 1993 ["How to Write a Proof"](/docs/math/1993-lamport.pdf):
> Anecdotal evidence suggests that as many as a third of all papers published in mathematical journals contain mistakes---not just minor errors, but incorrect theorems and proofs...My information about mathematicians' errors and embarrassment comes mainly from George Bergman.
[^Lamport-mistakes]: 1993 ["How to Write a Proof"](/docs/math/1993-lamport.pdf):
> Some twenty years ago, I decided to write a proof of the Schroeder-Bernstein theorem for an introductory mathematics class. The simplest proof I could find was in Kelley's classic general topology text [4, page 28]. Since Kelley was writing for a more sophisticated audience, I had to add a great deal of explanation to his half-page proof. I had written five pages when I realized that Kelley's proof was wrong. Recently, I wanted to illustrate a lecture on my proof style with a convincing incorrect proof, so I turned to Kelley. I could find nothing wrong with his proof; it seemed obviously correct! Reading and rereading the proof convinced me that either my memory had failed, or else I was very stupid twenty years ago. Still, Kelley's proof was short and would serve as a nice example, so I started rewriting it as a structured proof. Within minutes, I rediscovered the error.
>
> My interest in proofs stems from writing correctness proofs of algorithms. These proofs are seldom deep, but usually have considerable detail. Structured proofs provided a way of coping with this detail. The style was first applied to proofs of ordinary theorems in a paper I wrote with Martin Abadi [2]. He had already written conventional proofs|proofs that were good enough to convince us and, presumably, the referees. Rewriting the proofs in a structured style, we discovered that almost every one had serious mistakes, though the theorems were correct. Any hope that incorrect proofs might not lead to incorrect theorems was destroyed in our next collaboration [1]. Time and again, we would make a conjecture and write a proof sketch on the blackboard---a sketch that could easily have been turned into a convincing conventional proof---only to discover, by trying to write a structured proof, that the conjecture was false. Since then, I have never believed a result without a careful, structured proof. My skepticism has helped avoid numerous errors.
["How to Write a 21^st^ Century Proof"](https://www.microsoft.com/en-us/research/uploads/prod/2016/12/How-to-Write-a-21st-Century-Proof.pdf), Lamport 2011:
> My earlier paper on structured proofs described how effective they are at catching errors. It recounted how only by writing such a proof was I able to re-discover an error in a proof of the Schroeder-Bernstein theorem in a well-known topology text [2, page 28]. I recently received email from a mathematician saying that he had tried unsuccessfully to find that error by writing a structured proof. I asked him to send me his proof, and he responded:
>
>> I tried typing up the proof that I'd hand-written, and in the process, I think I've found the fundamental error. . . I now really begin to understand what you mean about the power of this method, even if it did take me hours to get to this point!
>
> It is instructive that, to find the error, he had to re-write his proof to be read by someone else. Eliminating errors requires care.
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](!Wikipedia), and one [would expect](http://www.codinghorror.com/blog/2006/07/diseconomies-of-scale-and-lines-of-code.html) [diseconomies of scale](!Wikipedia). 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](!Wikipedia) repository in 2007 contained [~323,551,126](http://debian-counting.libresoft.es/lenny/index.php?menu=Statistics) lines of code) that the number of active bugs at any time would be... fairly large. Mathematical software is hopefully better, but practitioners still run into issues (eg [Durán et al 2014](http://www.unirioja.es/cu/jvarona/downloads/DuranPerezVarona-trust.pdf "The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?"), [Fonseca et al 2017](https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf "An Empirical Study on the Correctness of Formally Verified Distributed Systems")) and I don't know of any research pinning down how buggy key mathematical systems like Mathematica are or how much published mathematics may be erroneous due to bugs.
This general problem led to predictions of doom and spurred much research into automated proof-checking, static analysis, and functional languages[^Hoare-1].
The doom, however, did not manifest and arguably operating systems & applications are more reliable in the 2000s+ than they were in the 1980--1990s[^Hoare-2] (eg. the general disappearance of the [Blue Screen of Death](!Wikipedia)). Users may not appreciate this point, but programmers who happen to think one day of just how the sausage of Gmail is made---how many interacting technologies and stacks of formats and protocols are involved---may get the shakes and wonder how it could *ever* work, much less be working at that moment. The answer is not really clear: it seems to be a combination of abundant computing resources driving down per-line error rates by avoiding optimization, modularization reducing interactions between lines, greater use of testing invoking an adversarial attitude to one's code, and a light sprinkling of formal methods & static checks[^Hoare-3].
[^Hoare-1]: ["How Did Software Get So Reliable Without Proof?"](/docs/math/1996-hoare.pdf), [C.A.R. Hoare](!Wikipedia) 1996:
> Twenty years ago it was reasonable to predict that the size and ambition of software products would be severely limited by the unreliability of their component programs. Crude estimates suggest that professionally written programs delivered to the customer can contain between one and ten independently correctable errors per thousand lines of code; and any software error in principle can have spectacular effect (or worse: a subtly misleading effect) on the behaviour of the entire system. Dire warnings have been issued..The arguments were sufficiently persuasive to trigger a significant research effort devoted to the problem of program correctness. A proportion of this research was based on the ideal of certainty achieved by mathematical proof.
[^Hoare-2]: Hoare 1996:
> Fortunately, the problem of program correctness has turned out to be far less serious than predicted. A recent analysis by Mackenzie has shown that of several thousand deaths so far reliably attributed to dependence on computers, only ten or so can be explained by errors in the software: most of these were due to a couple of instances of incorrect dosage calculations in the treatment of cancer by radiation. Similarly predictions of collapse of software due to size have been falsified by continuous operation of real-time software systems now measured in tens of millions of lines of code, and subjected to thousands of updates per year...And aircraft, both civil and military, are now flying with the aid of software measured in millions of lines---though not all of it is safety-critical. Compilers and operating systems of a similar size now number their satisfied customers in millions. So the questions arise: why have twenty years of pessimistic predictions been falsified? Was it due to successful application of the results of the research which was motivated by the predictions? How could that be, when clearly little software has ever has been subjected to the rigours of formal proof?
[^Hoare-3]: Hoare 1996:
> Success in the use of mathematics for specification, design and code reviews does not require strict formalisation of all the proofs. Informal reasoning among those who are fluent in the idioms of mathematics is extremely efficient, and remarkably reliable. It is not immune from failure; for example simple misprints can be surprisingly hard to detect by eye. Fortunately, these are exactly the kind of error that can be removed by early tests. More formal calculation can be reserved for the most crucial issues, such as interrupts and recovery procedures, where bugs would be most dangerous, expensive, and most difficult to diagnose by tests...Many more tests should be designed than there will ever be time to conduct; they should be generated as directly as possible from the specification, preferably automatically by computer program. Random selection at the last minute will protect against the danger that under pressure of time the program will be adapted to pass the tests rather than meeting the rest of its specification. There is some evidence that early attention to a comprehensive and rigorous test strategy can improve reliability of a delivered product, even when at the last minute there was no time to conduct the tests before delivery!
While hopeful, it's not clear how many of these would apply to existential risks: how does one use randomized testing on theories of existential risk, or tradeoff code clarity for computing performance?
## Type I vs Type II
So we might forgive case 1 errors entirely: if a community of mathematicians take an 'incorrect' proof about a particular existential risk and ratify it (either by verifying the proof subconsciously or seeing what their heuristics say), it not being written out because it would be tedious too[^Weiner], then we may be more confident in it[^Groupthink] than lumping the two error rates together. Case 2 errors are the problem, and they can sometimes be systematic. Most dramatically, when an entire group of papers with all their results turn out to be wrong since they made a since-disproved assumption:
> In the 1970s and 1980s, mathematicians discovered that framed manifolds with Arf-[Kervaire invariant](!Wikipedia) equal to 1---oddball manifolds not surgically related to a sphere---do in fact exist in the first five dimensions on the list: 2, 6, 14, 30 and 62. A clear pattern seemed to be established, and many mathematicians felt confident that this pattern would continue in higher dimensions...Researchers developed what Ravenel calls an entire "cosmology" of conjectures based on the assumption that manifolds with Arf-Kervaire invariant equal to 1 exist in all dimensions of the form $2^n - 2$. Many called the notion that these manifolds might not exist the "Doomsday Hypothesis," as it would wipe out a large body of research. Earlier this year, Victor Snaith of the University of Sheffield in England published a book about this research, warning in the preface, "...this might turn out to be a book about things which do not exist."
>
> Just weeks after Snaith's book appeared, Hopkins announced on April 21 that Snaith's worst fears were justified: that Hopkins, Hill and Ravenel had proved that no manifolds of Arf-Kervaire invariant equal to 1 exist in dimensions 254 and higher. Dimension 126, the only one not covered by their analysis, remains a mystery. The new finding is convincing, even though it overturns many mathematicians' expectations, Hovey said.^[["Mathematicians solve 45-year-old Kervaire invariant puzzle"](http://simonsfoundation.org/mathematics-physical-sciences/featured-articles/-/asset_publisher/bo1E/content/mathematicians-solve-45-year-old-kervaire-invariant-puzzle), Erica Klarreich 2009]
[^Weiner]: The missing steps may be quite difficult to fully prove, though; Nathanson 2009:
> There is a lovely but probably apocryphal anecdote about [Norbert Weiner](!Wikipedia). Teaching a class at MIT, he wrote something on the blackboard and said it was 'obvious.' One student had the temerity to ask for a proof. Weiner started pacing back and forth, staring at what he had written on the board and saying nothing. Finally, he left the room, walked to his office, closed the door, and worked. After a long absence he returned to the classroom. 'It *is* obvious', he told the class, and continued his lecture.
[^Groupthink]: What conditions count as full scrutiny by the math community may not be too clear; Nathanson 2009 trenchantly mocks math talks:
> Social pressure often hides mistakes in proofs. In a seminar lecture, for example, when a mathematician is proving a theorem, it is technically possible to interrupt the speaker in order to ask for more explanation of the argument. Sometimes the details will be forthcoming. Other times the response will be that it's "obvious" or "clear" or "follows easily from previous results." Occasionally speakers respond to a question from the audience with a look that conveys the message that the questioner is an idiot. That's why most mathematicians sit quietly through seminars, understanding very little after the introductory remarks, and applauding politely at the end of a mostly wasted hour.
The [parallel postulate](!Wikipedia "Parallel postulate#History") is another fascinating example of mathematical error of the second kind; its history is replete with false proofs even by greats like [Lagrange](!Wikipedia "Joseph Louis Lagrange") (on what strike the modern reader as bizarre grounds)[^Lagrange], self-deception, and misunderstandings---[Giovanni Girolamo Saccheri](!Wikipedia) developed a non-Euclidean geometry flawlessly but concluded it was flawed:
> The second possibility turned out to be harder to refute. In fact he was unable to derive a logical contradiction and instead derived many non-intuitive results; for example that triangles have a maximum finite area and that there is an absolute unit of length. He finally concluded that: "the hypothesis of the acute angle is absolutely false; because it is repugnant to the nature of straight lines". Today, his results are theorems of [hyperbolic geometry](!Wikipedia).
[^Lagrange]: ["Why Did Lagrange 'Prove' the Parallel Postulate?"](http://hans.math.upenn.edu/~kazdan/proof/notes/parallel-postulateGrabiner2009.pdf), Grabiner 2009:
> It is true that Lagrange never did publish it, so he must have realized there was something wrong. In another version of the story, told by [Jean-Baptiste Biot](!Wikipedia), who claims to have been there (though the minutes do not list his name), everybody there could see that something was wrong, so Lagrange's talk was followed by a moment of complete silence [2, p. 84]. Still, Lagrange kept the manuscript with his papers for posterity to read.
Why work on it at all?
> The historical focus on the fifth postulate came because it felt more like the kind of thing that gets proved. It is not self-evident, it requires a diagram even to explain, so it might have seemed more as though it should be a theorem. In any case, there is a tradition of attempted proofs throughout the Greek and then Islamic and then eighteenth-century mathematical worlds. Lagrange follows many eighteenth-century mathematicians in seeing the lack of a proof of the fifth postulate as a serious defect in [Euclid's _Elements_](!Wikipedia "Euclid's Elements"). But Lagrange's criticism of the postulate in his manuscript is unusual. He said that the assumptions of geometry should be demonstrable "just by the [principle of contradiction](!Wikipedia)"-the same way, he said, that we know the axiom that the whole is greater than the part [32, p. 30R]. The theory of parallels rests on something that is not self-evident, he believed, and he wanted to do something about this.
What was the strange and alien to the modern mind approach that Lagrange used?
> Recall that Lagrange said in this manuscript that axioms should follow from the principle of contradiction. But, he added, besides the principle of contradiction, "There is another principle equally self-evident," and that is Leibniz's [principle of sufficient reason](!Wikipedia). That is: nothing is true "unless there is a sufficient reason why it should be so *and not otherwise*" [42, p. 31; italics added]. This, said Lagrange, gives as solid a basis for mathematical proof as does the principle of contradiction [32, p. 30V]. But is it legitimate to use the principle of sufficient reason in mathematics? Lagrange said that we are justified in doing this, because it has already been done. For example, Archimedes [used it](!Wikipedia "Mechanical advantage#The law of the lever") to establish that equal weights at equal distances from the fulcrum of a lever balance. Lagrange added that we also use it to show that three equal forces acting on the same point along lines separated by a third of the circumference of a circle are in equilibrium [32, pp. 31R-31V]...The modern reader may object that Lagrange's symmetry arguments are, like the uniqueness of parallels, equivalent to Euclid's postulate. But the logical correctness, or lack thereof, of Lagrange's proof is not the point. (In this manuscript, by the way, Lagrange went on to give an analogous proof---also by the principle of sufficient reason-that between two points there is just one straight line, because if there were a second straight line on one side of the first, we could then draw a third straight line on the other side, and so on [32, pp. 34R-34V]. Lagrange, then, clearly liked this sort of argument.)
>
> ...Why did philosophers conclude that space had to be infinite, homogeneous, and the same in all directions? Effectively, because of the principle of sufficient reason. For instance, [Giordano Bruno](!Wikipedia) in 1600 argued that the universe must be infinite because there is no reason to stop at any point; the existence of an infinity of worlds is no less reasonable than the existence of a finite number of them. Descartes used similar reasoning in his _Principles of Philosophy_: "We recognize that this world. . . has no limits in its extension. . . . Wherever we imagine such limits, we . . . imagine beyond them some indefinitely extended space" [28, p. 104]. Similar arguments were used by other seventeenth-century authors, including Newton. Descartes identified space and the extension of matter, so geometry was, for him, about real physical space. But geometric space, for Descartes, had to be Euclidean...Descartes, some 50 years before Newton published his first law of motion, was a co-discoverer of what we call linear inertia: that in the absence of external influences a moving body goes in a straight line at a constant speed. Descartes called this the first law of nature, and for him, this law follows from what we now recognize as the principle of sufficient reason. Descartes said, "Nor is there any reason to think that, if [a part of matter] moves. . . and is not impeded by anything, it should ever by itself cease to move with the same force" [30, p. 75]...Leibniz, by contrast, did not believe in absolute space. He not only said that spatial relations were just the relations between bodies, he used the principle of sufficient reason to show this. If there were absolute space, there would have to be a reason to explain why two objects would be related in one way if East is in one direction and West in the opposite direction, and related in another way if East and West were reversed [24, p. 147]. Surely, said Leibniz, the relation between two objects is just one thing! But Leibniz did use arguments about symmetry and sufficient reason-sufficient reason was his principle, after all. Thus, although Descartes and Leibniz did not believe in empty absolute space and Newton did, they all agreed that what I am calling the Euclidean properties of space are essential to physics.
>
> ...In his 1748 essay ["Reflections on Space and Time"](http://eulerarchive.maa.org/docs/translations/E149tr.pdf), Euler argued that space must be real; it cannot be just the relations between bodies as the Leibnizians claim [10]. This is because of the principles of mechanics---that is, Newton's first and second laws. These laws are beyond doubt, because of the "marvelous" agreement they have with the observed motions of bodies. The inertia of a single body, Euler said, cannot possibly depend on the behavior of other bodies. The conservation of uniform motion in the same direction makes sense, he said, only if measured with respect to immovable space, not to various other bodies. And space is not in our minds, said Euler; how can physics-real physics-depend on something in our minds?...in his _[Critique of Pure Reason](!Wikipedia)_ of 1781, Kant placed space in the mind nonetheless. We order our perceptions in space, but space itself is in the mind, an intuition of the intellect. Nevertheless, Kant's space turned out to be Euclidean too. Kant argued that we need the intuition of space to prove theorems in geometry. This is because it is in space that we make the constructions necessary to prove theorems. And what theorem did Kant use as an example? The sum of the angles of a triangle is equal to two right angles, a result whose proof requires the truth of the parallel postulate [26, "Of space," p. 423]...Lagrange himself is supposed to have said that spherical trigonometry does not need Euclid's parallel postulate [4, pp. 52--53]. But the surface of a sphere, in the eighteenth-century view, is not non-Euclidean; it exists in 3-dimensional Euclidean space [20, p. 71]. The example of the sphere helps us see that the eighteenth-century discussion of the parallel postulate's relationship to the other postulates is not really about what is logically possible, but about what is true of real space.
The final step:
> [Johann Heinrich Lambert](!Wikipedia) was one of the mathematicians who worked on the problem of Postulate 5. Lambert explicitly recognized that he had not been able to prove it, and considered that it might always have to remain a postulate. He even briefly suggested a possible geometry on a sphere with an imaginary radius. But Lambert also observed that the parallel postulate is related to the law of the lever [20, p. 75]. He said that a lever with weightless arms and with equal weights at equal distances is balanced by a force in the opposite direction at the center equal to the sum of the weights, and that all these forces are parallel. So either we are using the parallel postulate, or perhaps, Lambert thought, some day we could use this physical result to prove the parallel postulate...These men did not want to do mechanics, as, say, Newton had done. They wanted to show not only that the world was this way, but that it necessarily had to be. A modern philosophical critic, Helmut Pulte, has said that Lagrange's attempt to "reduce" mechanics to analysis strikes us today as "a misplaced endeavour to mathematize. . . an empirical science, and thus to endow it with infallibility" [39, p. 220]. Lagrange would have responded, "Right! That's just exactly what we are all doing."
We could look upon Type II errors as having a benevolent aspect: they show both that our existing methods are too weak & informal *and* that our intuition/heuristics break down at it---implying that all previous mathematical effort has been *systematically* misled in avoiding that area (as empty), and that there is much low-hanging fruit. (Consider how many scores or hundreds of key theorems were proven by the very first mathematicians to work in the non-Euclidean geometries!)
# Future implications
Should such widely-believed conjectures as [P ≠ NP](!Wikipedia "P=NP")[^Lipton-2] or the [Riemann hypothesis](!Wikipedia) turn out be false, then because they are assumed by so many existing proofs, entire textbook chapters (and perhaps textbooks) would disappear---and our previous estimates of error rates will turn out to have been substantial underestimates.
But it may be a cloud with a silver lining: it is not what you don't know that's dangerous, but what you know that ain't so.
[^Lipton-2]: [Supposing P=NP](http://rjlipton.wordpress.com/2012/09/29/why-we-lose-sleep-some-nights/ "Why We Lose Sleep Some Nights"):
> Much of CS theory would disappear. In my own research some of Ken's and my "best" results would survive, but many would be destroyed. The Karp-Lipton Theorem is gone in this world. Ditto all "dichotomy" results between P and NP-complete, and for P = #P, Jin-Yi's similar work. Many barrier results, such as oracle theorems and natural proofs, lose their main motivation, while much fine structure in hardness-versus-randomness tradeoffs would be blown up. The PCP Theorem and all the related work is gone. Modern cryptography could survive if the algorithm were galactic, but otherwise would be in trouble. I am currently teaching Complexity Theory at Tech using the textbook by Sanjeev Arora and Boaz Barak...Most of the 573 pages of Arora-Barak would be gone:
>
> - Delete all of chapter 3 on NP.
> - Delete all of chapter 5 on the polynomial hierarchy.
> - Delete most of chapter 6 on circuits.
> - Delete all of chapter 7 on probabilistic computation.
> - Mark as dangerous chapter 9 on cryptography.
> - Delete most of chapter 10 on quantum computation---who would care about Shor's algorithm then?
> - Delete all of chapter 11 on the PCP theorem.
>
> I will stop here. Most of the initial part of the book is gone. The same for much of Homer-Selman, and basically all of the "Reducibility and Completeness" CRC chapter.
# See Also
- [One man's modus ponens is another man's modus tollens](/Modus)
# External Links
- ["Confidence levels inside and outside an argument"](http://lesswrong.com/lw/3be/confidence_levels_inside_and_outside_an_argument/)
- [_An Essay on the Psychology of Invention in the Mathematical Field_](https://archive.org/details/eassayonthepsych006281mbp) ([Jacques Hadamard](!Wikipedia); 1945)
- "[The Unreasonable Effectiveness of Mathematics in the Natural Sciences](!Wikipedia)", Wigner 1960; ["The Unreasonable Effectiveness of Mathematics"](https://www.dartmouth.edu/~matc/MathDrama/reading/Hamming.html), Richard Hamming 1980
- ["LA-602: Ignition of the Atmosphere with Nuclear Bombs"](http://www.sciencemadness.org/lanl1_a/lib-www/la-pubs/00329010.pdf) (["LA-602 vs. RHIC Review"](http://lesswrong.com/lw/rg/la602_vs_rhic_review/))
- Responses:
- ["Flaws in the Perfection"](http://www.aleph.se/andart/archives/2012/09/flaws_in_the_perfection.html) -(Anders Sandberg commentary on this essay)
- [Hacker News discussion](https://news.ycombinator.com/item?id=6500577)
- ["Bounding the impact of AGI"](http://lesswrong.com/r/discussion/lw/fzc/bounding_the_impact_of_agi/)
- ["Mathematical Proofs Improve But Don't Guarantee Security, Safety, and Friendliness"](http://intelligence.org/2013/10/03/proofs/) (Luke Muehlhauser)
- ["The probabilistic heuristic justification of the ABC conjecture"](https://terrytao.wordpress.com/2012/09/18/the-probabilistic-heuristic-justification-of-the-abc-conjecture/) (Terence Tao)
- ["Could We Have Felt Evidence For SDP ≠ P?"](http://rjlipton.wordpress.com/2014/03/15/could-we-have-felt-evidence-for-sdp-p/) (see particularly "Bad Guesses")
- ["Have any long-suspected irrational numbers turned out to be rational?"](http://mathoverflow.net/questions/32967/have-any-long-suspected-irrational-numbers-turned-out-to-be-rational); ["Mathematical 'urban legends'"](http://mathoverflow.net/questions/53122/mathematical-urban-legends); ["Examples of falsified (or currently open) longstanding conjectures leading to large bodies of incorrect results"](https://math.stackexchange.com/questions/347460/examples-of-falsified-or-currently-open-longstanding-conjectures-leading-to-la); ["What mistakes did the Italian algebraic geometers actually make?"](https://mathoverflow.net/questions/19420/what-mistakes-did-the-italian-algebraic-geometers-actually-make); ["Why doesn't mathematics collapse down, even though humans quite often make mistakes in their proofs?"](https://mathoverflow.net/questions/338607/why-doesnt-mathematics-collapse-down-even-though-humans-quite-often-make-mista); ["Most interesting mathematics mistake?"](https://mathoverflow.net/questions/879/most-interesting-mathematics-mistake)
- ["In Mathematics, Mistakes Aren't What They Used To Be: Computers can't invent, but they're changing the field anyway"](http://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be)
- ["Cosmic Rays: what is the probability they will affect a program?"](https://stackoverflow.com/questions/2580933/cosmic-rays-what-is-the-probability-they-will-affect-a-program) or [GUIDs](https://blogs.msdn.microsoft.com/oldnewthing/20160114-00/?p=92851 "When you start talking about numbers as small as 2⁻¹²², you have to start looking more closely at the things you thought were zero")
- ["Another Look at Provable Security"](http://cacr.uwaterloo.ca/~ajmeneze/anotherlook/index.shtml)
- ["Verifier Theory and Unverifiability"](https://arxiv.org/ftp/arxiv/papers/1609/1609.00331.pdf), Yampolskiy 2016
- "[What the Tortoise Said to Achilles](!Wikipedia)"
- ["Burn-in, bias, and the rationality of anchoring"](https://pdfs.semanticscholar.org/4ee1/0c751d68aa737cd89e561a4b474e6806188c.pdf), Lieder et al 2012; ["Where Do Hypotheses Come From?"](http://gershmanlab.webfactional.com/pubs/Dasgupta17.pdf), Dasgupta et al 2017
- ["Fast-key-erasure random-number generators"](https://blog.cr.yp.to/20170723-random.html "2017.07.23: Fast-key-erasure random-number generators An effort to clean up several messes simultaneously. #rng #forwardsecrecy #urandom #cascade #hmac #rekeying #proofs"), Dan Bernstein
- ["7.2.1.7: History of Combinatorial Generation"](http://www.antiquark.com/blogimg/fasc4b.pdf), Knuth
- ["Proofs shown to be wrong after formalization with proof assistant?"](https://mathoverflow.net/questions/291158/proofs-shown-to-be-wrong-after-formalization-with-proof-assistant/)
- ["Problem Solving"](http://www.compilerpress.ca/Competitiveness/Anno/Anno%20Polanyi%20Problem%20Solving%20BJPS%201957.htm), Polanyi 1957
- ["Bloom filters debunked: Dispelling 30 Years of bad math with Coq!"](https://gopiandcode.uk/logs/log-bloomfilters-debunked.html) ("The widely cited expression for the false positive rate of a bloom filter is wrong! In fact, as it turns out, the behaviours of a Bloom filter have actually been the subject of 30 years of mathematical contention, requiring *multiple* corrections and even *corrections of these corrections*.")
- ["How Close Are Computers to Automating Mathematical Reasoning? AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine"](https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/)
- ["When Extrapolation Fails Us: Incorrect Mathematical Conjectures [About Very Large Numbers]"](http://www.wired.com/2014/09/when-extrapolation-fails-us/)
- ["Patterns that Eventually Fail"](https://johncarlosbaez.wordpress.com/2018/09/20/patterns-that-eventually-fail/) (on [Borwein integrals](!Wikipedia "Borwein integral"): [Borwein & Borwein 2001](/docs/math/2001-borwein.pdf "Some Remarkable Properties of Sinc and Related Integrals"); $2 \cdot cos(t)$ [example](/images/statistics/borweinintegral-2cost.jpg){.invertible} from [Schmid 2014](/docs/math/2014-schmid.pdf "Two curious integrals and a graphic proof"))
# Appendix
## Jones 1998
"A credo of sorts"; Vaughan Jones ([_Truth in Mathematics_](/docs/math/1998-dales-truthinmathematics.pdf), 1998), pg208--209:
> *Proofs are indispensable, but I would say they are necessary but not sufficient for mathematical truth, at least truth as perceived by the individual.*
>
> To justify this attitude let me invoke two experiences of current mathematics, which very few mathematicians today have escaped.
>
> The first is computer programming. To write a short program, say 100 lines of C code, is a relatively painless experience. The debugging will take longer than the writing, but it will not entail suicidal thoughts. However, should an inexperienced programmer undertake to write a slightly longer program, say 1000 lines, distressing results will follow. The debugging process becomes an emotional nightmare in which one will doubt one's own sanity. One will certainly insult the compiler in words that are inappropriate for this essay. The mathematician, having gone through this torture, cannot but ask: "Have I ever subjected the proofs of any of my theorems to such close scrutiny?" In my case at least the answer is surely "no". So while I do not doubt that my proofs are correct (at least the significant ones), my belief in the results needs bolstering. Compare this with the debugging process. At the end of debugging we are happy with our program because of the consistency of the output it gives, not because we feel we have proved it correct---after all we did that at least twenty times while debugging and we were wrong *every time*. Why not a twenty-first? In fact we are acutely aware that our poor program has only been tested with a limited set of inputs and we fully expect more bugs to manifest themselves when inputs are used which we have not yet considered. If the program is sufficiently important, it will be further debugged in the course of time until it becomes secure with respect to all inputs. (With much larger programs this will never happen.) So it is with our theorems. Although we may have proofs galore and a rich surrounding structure, if the result is at all difficult it is only the test of time that will cause acceptance of the "truth" of the result.
>
> The second experience concerning the need for supplements to proof is one which I used to dislike intensely, but have come to appreciate and even search for. It is the situation where one has two watertight, well-designed arguments---that lead inexorably to opposite conclusions. Remember that research in mathematics involves a foray into the unknown. We may not know which of the two conclusions is correct or even have any feeling or guess. Proof at this point is our only arbiter. And it seems to have let us down. I have known myself to be in this situation for months on end. It induces obsessive and anti-social behaviour. Perhaps we have found an inconsistency in mathematics. But no, eventually some crack is seen in one of the arguments and it begins to look more and more shaky. Eventually we kick ourselves for being so utterly stupid and life goes on. But it was no tool of logic that saved us. The search for a chink in the armour often involved many tricks including elaborate thought experiments and perhaps computer calculations. Much structural understanding is created, which is why I now so value this process. One's feeling of having obtained truth at the end is approaching the absolute. Though I should add that I have been forced to reverse the conclusion on occasions...