http://arxiv.org/pdf/1302.2898v1.pdf
"Where stands the mathematical endeavor? In 2012, many mathematical utilities are reaching consolidation. It is an age of large aggregates and large repositories of mathematics: the arXiv, Math Reviews, and euDML, which promises to aggregate the many European archives such as Zentralblatt Math and Numdam. Sage aggregates dozens of mathematically oriented computer programs under a single Python-scripted front-end. Book sales in the U.S. have been dropping for the past several years. Instead, online sources such as Wikipedia and Math Overflow are rapidly becoming students' preferred math references. The Polymath blog organizes massive mathematical collaborations. Other blogs organize previously isolated researchers into new fields of research. The slow, methodical deliberations of referees in the old school are giving way; now in a single stroke, Tao blogs, gets feedback, and publishes.
Machine Learning is in its ascendancy. LogAnswer and Wolfram Alpha answer our elementary questions about the quantitative world; Watson our Jeopardy questions. Google Page ranks our searches by calculating the largest eigenvalue of the largest matrix the world has ever known. Deep Blue plays our chess games. The million-dollar-prize-winning Pragmatic Chaos algorithm enhances our Netflix searches. The major proof assistants now contain tens of thousands of formal proofs that are being mined for hints about how to prove the next generation of theorems.
Mathematical models and algorithms rule the quantitative world. Without applied mathematics, we would be bereft of Shor's factorization algorithm for quantum computers, Yang-Mills theories of strong interactions in physics, invisibility cloaks, Radon transforms for medical imaging, models of epidemiology, risk analysis in insurance, stochastic pricing models of financial derivatives, RSA encryption of sensitive data, Navier-Stokes modeling of fluids, and models of climate change. Without it, entire fields of engineering from Control Engineering to Operations Research would close their doors. The early icon of mathematical computing, Von Neumann, divided his final years between meteorology and hydrogen bomb calculations. Today, applications fuel the economy: in 2011 rankings, the first five of the "10 best jobs" are math or computer related: software engineer, mathematician, actuary, statistician, and computer systems analyst [CC111].
Computers have rapidly become so pervasive in mathematics that future generations may look back to this day as a golden dawn. A comprehensive survey is out of the question. It would almost be like asking for a summary of applications of symmetry to mathematics. Computability - like symmetry - is a wonderful structural property that some mathematical objects possess that makes answers flow more readily wherever it is found.
It has become common for problems in mathematics to be first verified by computer and later confirmed without them. Some examples are the construction of sporadic groups, counterexamples to a conjecture of Euler, the proof of the Catalan conjecture, and the discovery of a formula for the binary digits of π.
Perhaps the best known example is the construction of sporadic groups as part of the monumental classification of finite simple groups. The sporadic groups are the 26 finite simple groups that do not fall into natural infinite families. For example, Lyons 1972) predicted the existence of a sporadic group of order
2 8 · 3 7 · 5 6 · 7 · 11 · 31 · 37 · 67.
In 1973, Sims proved the existence of this group in a long unpublished manuscript that relied on many specialized computer programs. By 1999 , the calculations had become standardized in group theory packages, such as GAP and Magma [HS99]. Eventually, computer-free existence and uniqueness proofs were found [MC02], [AS92].
Euler conjectured (1769) that a fourth power cannot be the sum of three positive fourth powers, that a fifth power cannot be the sum of four positive fifth powers, and so forth. In 1966, a computer search [LP66] on a CDC 6600 mainframe uncovered a counterexample:
27^5 + 84^5 + 110^5 + 133^5 = 144^5 ,
which can be checked by hand (I dare you). The two-sentence announcement of this counterexample qualifies as one of the shortest mathematical publications of all times.
The Catalan conjecture (1844) asserts that the only solution to the equation
x^m − y^n = 1,
in positive integers x, y, m, n with exponents m, n greater than 1 is the obvious
3^2 − 2^3 = 1.
That is, 8 and 9 are the only consecutive positive perfect powers. By the late 1970s, Baker's methods in Diophantine analysis had reduced the problem to an astronomically large and hopelessly infeasible finite computer search. Mih ̆ailescu's proof (2002) of the Catalan conjecture made light use of computers (a one-minute calculation), and later the computer calculations were entirely eliminated [Mih04], [Met03].
Bailey, Borwein, and Plouffe found an algorithm for calculating the nth binary digit of π directly: it jumps straight to the nth digit without first calculating any of the earlier digits. They understood that to design such an algorithm, they would need an infinite series for π in which powers of 2 controlled the denominators. They did not know of any such formula, and made a computer search (using the PSLQ lattice reduction algorithm) for any series of the desired form. Their search unearthed a numerical identity
! ! n ∞ X 2 1 1 1 4 − − − , π = 8n + 1 8n + 4 8n + 5 8n + 6 16 n=0
which was then rigorously proved and used to implement their binary-digits algorithm.
until recently, no arrangements of regular tetrahedra with high density were known to exist. In 2000, Betke and Henk developed an efficient computer algorithm to find the densest lattice packing of a general convex body [BH00]. This opened the door to experimentation [CT06]. For example, the algorithm can determine the best lattice packing of the convex hull of the cluster of tetrahedra in Figure 3. In rapid succession came new record-breaking arrangements of tetrahedra, culminating in what is now conjectured to be the best possible [CEG10]. (See Figure 4.) Although Chen had the panache to hand out Dungeons and Dragons tetrahedral dice to the audience for a hands-on modeling session during her thesis defense, the best arrangement7 was found using Monte Carlo experiments. In the numerical simulations, a finite number of tetrahedra are randomly placed in a box of variable shape. The tetrahedra are jiggled as the box slowly shrinks until no further improvement is possible. Now that a precise conjecture has been formulated, the hardest part still remains: to give a proof.
L. Fejes Toth proposed a strategy to prove Kepler's conjecture in the 1950s, and later he suggested that computers might be used. The proof, finally obtained by Ferguson and me in 1998, is one of the most difficult nonlinear optimization problems ever rigorously solved by computer [Hal05b]. The computers calculations originally took about 2000 hours to run on Sparc workstations. Recent simplifications in the proof have reduced the runtime to about 20 hours and have reduced the amount of customized code by a factor of more than 10.
The four-color theorem is the most celebrated computer proof in the history of mathematics.
The conjecture is that every finite projective plane of order n > 1 is a prime power. The smallest integers n > 1 that are not prime powers are
6, 10, 12, 14, 15, . . .
The brute force approach to this conjecture is to eliminate each of these possibilities in turn. The case n = 6 was settled in 1938. Building on a number of theoretical advances [MST73], Lam eliminated the case n = 10 in 1989, in one of the most difficult computer proofs in history [LTS89]. This calculation was executed over a period of years on multiple machines and eventually totaled about 2000 hours of Cray-1A time. Unlike the computer proof of the four-color theorem, the projective plane proof has never received independent verification. Because of the possibilities of programming errors and soft errors (see Section 3.5), Lam is unwilling to call his result a proof. He writes, "From personal experience, it is extremely easy to make programming mistakes. We have taken many precautions, . . . Yet, I want to emphasize that this is only an experimental result and it desperately needs an independent verification, or better still, a theoretical explanation" [Lam91]. Recent speculation at Math Overflow holds that the next case, n = 12, remains solidly out of computational reach [Hor10].
Lorenz conjectured in 1963 that his oscillator has a strange attractor (Figure 7). In 1982, the Lax report cited soliton theory and strange attractors as two prime examples of the "discovery of new phenomena through numerical experimentation," and calls such discovery perhaps the most "significant application of scientific computing" [Lax82]. Smale, in his list of 18 "Mathematical Problems for the Next Century" made the fourteenth problem to present a rigorous proof that the dynamics of the Lorenz oscillator is a strange attractor [Sma98] with various additional properties that make it a "geometric Lorenz attractor."
Tucker has solved Smale's fourteenth problem by computer [Tuc02] [Ste00]. One particularly noteworthy aspect of this work is that chaotic systems, by their very nature, pose particular hardships for rigorous computer analysis. Nevertheless, Tucker implemented the classical Euler method for solving ordinary differential equations with particular care, using interval arithmetic to give mathematically rigorous error bounds. Tucker has been awarded numerous prizes for this work, including the Moore Prize (2002) and the EMS Prize (2004).
Mandelbrot's conjectures in fractal geometry have resulted in two Fields Medals. Here he describes the discovery of the 4/3-conjecture made in [Man82]. "The notion that these conjectures might have been reached by pure thought - with no picture - is simply inconceivable.. . . I had my programmer draw a very big sample [Brownian] motion and proceeded to play with it." He goes on to describe computer experiments that led him to enclose the Brownian motion into black clusters that looked to him like islands with jagged coastlines (Figure 8). "instantly, my long previous experience with the coastlines of actual islands on Earth came handy and made me suspect that the boundary of Brownian motion has a fractal dimension equal to 4/3" [Man04]. This conjecture, which Mandelbrot's trained eye spotted in an instant, took 18 years to prove [LSW01].
Smale (1958) proved that it is possible to turn a sphere inside out without introducing any creases. 2 For a long time, this paradoxical result defied the intuition of experts...The computer videos of this theorem are spectacular. Watch them on YouTube! As we watch the sphere turn inside out, our intuition grows. The computer calculations behind the animations of the first video (the Optiverse) start with a sphere, half inverted and half right-side out [SFL]. From halfway position, the path of steepest descent of an energy functional is used to calculate the unfolding in both directions to the round spheres, with one fully inverted (Figure 9). The second video is based on Thurston's "corrugations" [LMM94]. As the name suggests, this sphere eversion has undulating ruffles that dance like a jellyfish, but avoids sharp creases. Through computers, understanding.
Weber and Wolf [WW11] report that the use of computer visualization has become "commonplace" in minimal surface research, "a conversation between visual aspects of the minimal surfaces and advancing theory, each supporting the other." This started when computer illustrations of the Costa surface (a particular minimal surface, Figure 10) in the 1980s revealed dihedral symmetries of the surface that were not seen directly from its defining equations. The observation of symmetry turned out to be the key to the proof that the Costa surface is an embedding. The symmetries further led to a conjecture and then proof of the existence of other minimal surfaces of higher genus with similar dihedral symmetries. As Hoffman wrote about his discoveries, "The images produced along the way were the objects that we used to make discoveries. They are an integral part of the process of doing mathematics, not just a way to convey a discovery made without their use" [Hof87].
As explained above, six is the kissing number in two dimensions, 240 is the kissing number in eight dimensions. In three dimensions, the kissing number is 12. This three-dimensional problem goes back to a discussion between Newton and Gregory in 1694, but was not settled until the 1950s. A recent computer proof makes an exhaustive search through nearly 100 million combinatorial possibilities to determine exactly how much the twelve spheres must shrink to accommodate a thirteenth [MT10]. Bachoc and Vallentin were recently awarded the SIAG/Optimization prize for their use of semi-definite programming algorithms to establish new proofs of the kissing number in dimensions 3, 4, 8 and new bounds on the kissing number in various other dimensions [BV08].
At the close of this first section, we confess that a survey of mathematics in the age of the Turing machine is a reckless undertaking, particularly if it almost completely neglects software products and essential mathematical algorithms - the Euclidean algorithm, Newton's method, Gaussian elimination, fast Fourier transform, simplex algorithm, sorting, Sch ̈onhage-Strassen, and many more.
Year Theorem Proof System Formalizer Traditional Proof
1986 First Incompleteness Shankar Goedel
1990 Quadratic Reciprocity Russinoff Eisenstein
1996 Fundamental - of Calculus Harrison Henstock
2000 Fundamental - of Algebra Milewski Brynski
2000 Fundamental - of Algebra Geuvers et al Kneser
2004 Four Color Gonthier Robertson et al.
2004 Prime Number Avigad et al. Selberg-Erd ̈os
2005 Jordan Curve Hales Thomassen
2005 Brouwer Fixed Point Harrison Kuhn
2006 Flyspeck I Bauer-Nipkow Hales
2007 Cauchy Residue Harrison classical
2008 Prime Number Harrison analytic proof
2012 Odd Order Theorem Gonthier Feit-Thompson
Writing about first-order automated reasoning, Huet and Paulin-Mohring [BC04] describe the situation in the early 1970s as a "catastrophic state of the art." "The standard mode of use was to enter a conjecture and wait for the computer's memory to exhaust its capacity. Answers were obtained only in exceptionally trivial cases." They go on to describe numerous developments (Knuth-Bendix, LISP, rewriting technologies, LCF, ML, Martin-L ̈of type theory, NuPrl, Curry-Howard correspondence, dependent types, etc.) that led up to the Coq proof assistant. These developments led away from first-order theorem proving with its "thousands of unreadable logical consequences" to a highly structured approach to theorem proving in Coq.
First-order theorem proving has developed significantly over the years into sophisticated software products. They are no longer limited to "exceptionally limited cases." Many different software products compete in an annual competition (CASC), to see which can solve difficult first-order problems the fastest. The LTB (large theory batch) division of the competition includes problems with thousands of axioms [PSST08]. Significantly, this is the same order of magnitude as the total number of theorems in a proof assistant. What this means is that a first-order theorem provers have reached the stage of development that they might be able to give fully automated proofs of new theorems in a proof assistant, working from the full library of previously proved theorems. sledgehammer. The Sledgehammer tactic is Paulson's implementation of this idea of full automation in the Isabelle/HOL proof assistant [Pau10]. As the name 'Sledgehammer' suggests, the tactic is all-purpose and powerful, but demolishes all higher mathematical structure, treating every goal as a massive unstructured problem in first-order logic. If L is the set of all theorems in the Isabelle/HOL library, and g is a goal, it would be possible to hand off the problem L =⇒ g to a first-order theorem prover. However, success rates are dramatically improved, when the theorems in L are first assessed by heuristic rules for their likely relevance for the goal g, in a process called relevance filtering. This filtering is used to reduce L to an axiom set L 0 of a few hundred theorems that are deemed most likely to prove g.
The problem L 0 =⇒ g is stripped of type information, converted to a first-order, and fed to first-order theorem provers. Experiments indicate that it is more effective to feed a problem in parallel into multiple first-order provers for a five-second burst than to hand the problem to the best prover (Vampire) for a prolonged attack [Pau10], [BN10]. When luck runs in your favor, one of the first-order theorem provers finds a proof. The reconstruction of a formal proof from a first-order proof can encounter hurdles. For one thing, when type information is stripped from the problem (which is done to improve performance), soundness is lost. "In unpublished work by Urban, MaLARea [a machine learning program for relevance ranking] easily proved the full Sledgehammer test suite by identifying an inconsistency in the translated lemma library; once MaLARea had found the inconsistency in one proof, it easily found it in all the others" [Pau10], [Urb07]
...B ̈ohme and Nipkow took 1240 proof goals that appear in several diverse theories of the Isabelle/HOL system and ran sledgehammer on all of them [BN10]. The results are astounding. The success rate (of obtaining fully reconstructed formal proofs) when three different first-order provers run for two-minutes each was 48%. The proofs of these same goals by hand might represent years of human labor, now fully automated through a single new tool. Sledgehammer has led to a new style of theorem proving, in which the user is primarily responsible for stating the goals. In the final proof script, there is no explicit mention of sledgehammer. Metis proves the goals, with sledgehammer operating silently in the background to feed metis with whatever theorems it needs. For example, a typical proof script might contain lines such as [Pau10] hence "x ⊆ space M" by (metis sets into space lambda system sets)
The first line is the goal that the user types. The second line has been automatically inserted into the proof script by the system, with the relevant theorems sets, into etc. selected by Sledgehammer.
The Feit-Thompson theorem, or odd-order theorem, is one of the most significant theorems of the twentieth century. (For his work, Thompson was awarded the three highest honors in the mathematical world: the Fields Medal, the Abel Prize, and the Wolf Prize.) The Feit-Thompson theorem states that every finite simple group has even order, except for cyclic groups of prime order. The proof, which runs about 250 pages, is extremely technical. The Feit-Thompson theorem launched the endeavor to classify all finite simple groups, a monumental undertaking that consumed an entire generation of group theorists.
Gonthier's team has formalized the proof of the Feit-Thompson theorem [Gon12]. To me as a mathematician, nothing else that has been done by the formal proof community compares in splendor to the formalization of this theorem.
To explain the concept of separation of concerns, Dijkstra tells the story of an old initiative to create a new programming language that failed miserably because the designers felt that the new language had to look just like FORTRAN to gain broad acceptance. "The proper technique is clearly to postpone the concerns for general acceptance until you have reached a result of such a quality that it deserves acceptance" [Dij82].
For a long time, proof formalization technology was unable to advance beyond the mathematics of the 19th century, picking classical gems such as the Jordan curve theorem, the prime number theorem, or Dirichlet's theorem on primes in arithmetic progressions. With the Feit-Thompson theorem, formalization has risen to a new level, by taking on the work of a Fields medalist.
At this level, there is an abundant supply of mathematical theorems to choose from. A Dutch research agenda lists the formalization of Fermat's Last Theorem as the first in a list of "Ten Challenging Research Problems for Computer Science" [Ber05]. Hesselink predicts that this one formalization project alone will take about "fifty years, with a very wide margin." Small pieces of the proof of Fermat, such as class field theory, the Langlands-Tunnell theorem, or the arithmetic theory of elliptic curves would be a fitting starting point. The aim is to develop technologies until formal verification of theorems becomes routine at the level of Atiyah-Singer index theorem, Perelman's proof of the Poincar ́e conjecture, the Green-Tao theorem on primes in arithmetic progression, or Ngˆo's proof of the fundamental lemma.
Why use computers to verify mathematics? The simple answer is that carefully implemented proof checkers make fewer errors than mathematicians (except J.-P. Serre). Incorrect proofs of correct statements are so abundant that they are impossible to catalogue. Ralph Boas, former executive editor of Math Reviews, once remarked that proofs are wrong "half the time" [Aus08]. Kempe's claimed proof of the four-color theorem stood for more than a decade before Heawood refuted it [Mac01, p. 115]. "More than a thousand false proofs [of Fermat's Last Theorem] were published between 1908 and 1912 alone" [Cor10]. Many published theorems are like the hanging chad ballots of the 2000 U.S. presidential election, with scrawls too ambivalent for a clear yea or nay. One mathematician even proposed to me that a new journal is needed that unlike the others only publishes reliable results. Euclid gave us a method, but even he erred in the proof of the very first proposition of the Elements when he assumed without proof that two circles, each passing through the other's center, must intersect. The concept that is needed to repair the gap in Euclid's reasoning is an intermediate value theorem. This defect was not remedied until Hilbert's 'Foundations of Geometry.' Examples of widely accepted proofs of false or unprovable statements show that our methods of proof-checking are far from perfect. Lagrange thought he had a proof of the parallel postulate, but had enough doubt in his argument to withhold it from publication. In some cases, entire schools have become sloppy, such as the Italian school of algebraic geometry or real analysis before the revolution in rigor towards the end of the nineteenth century. Plemelj's 1908 accepted solution to Hilbert's 21st problem on the monodromy of linear differential equations was refuted in 1989 by Bolibruch. Auslander gives the example of a theorem 12 published by Waraskiewicz in 1937, generalized by Choquet in 1944, then refuted with a counterexample by Bing in 1948 [Aus08]. Another example is the approximation problem for Sobolev maps between two manifolds [Bet91], which contains a faulty proof of an incorrect statement. The corrected theorem appears in [HL03]. Such examples are so plentiful that a Wiki page has been set up to classify them, with references to longer discussions at Math Overflow [Wik11], [Ove09], [Ove10].
Theorems that are calculations or enumerations are especially prone to error. Feynman laments, "I don't notice in the morass of things that something, a little limit or sign, goes wrong.. . . I have mathematically proven to myself so many things that aren't true" [Fey00, p. 885]. Elsewhere, Feynman describes two teams of physicists who carried out a two-year calculation of the electron magnetic moment and independently arrived at the same predicted value. When experiment disagreed with prediction, the discrepancy was eventually traced to an arithmetic error made by the physicists, whose calculations were not so independent as originally believed [Fey85, p. 117]. Pontryagin and Rokhlin erred in computing stable homotopy groups of spheres. Little's tables of knots from 1885 contains duplicate entries that went undetected until 1974. In enumerative geometry, in 1848, Steiner counted 7776 plane conics tangent to 5 general plane conics, when there are actually only 3264. One of the most persistent blunders in the history of mathematics has been the misclassification (or misdefinition) of convex Archimedean polyhedra. Time and again, the pseudo rhombic cuboctahedron has been overlooked or illogically excluded from the classification (Figure 21) [Gr ̈u11].
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 FIT}{1Mbit} * 64GB * 77 hours = \frac{10^3 errors}{10^9 hours Mbit} * (64 * 8 * 10^3 Mbit) * 77 hours ≈ 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."
This makes perhaps the third instance I've seen today of Amara's law: formal proofs, neural networks (http://www.wired.com/2014/08/deep-learning-yann-lecun/), and paperless offices (http://crookedtimber.org/2014/08/13/origami/).
"Where stands the mathematical endeavor? In 2012, many mathematical utilities are reaching consolidation. It is an age of large aggregates and large repositories of mathematics: the arXiv, Math Reviews, and euDML, which promises to aggregate the many European archives such as Zentralblatt Math and Numdam. Sage aggregates dozens of mathematically oriented computer programs under a single Python-scripted front-end. Book sales in the U.S. have been dropping for the past several years. Instead, online sources such as Wikipedia and Math Overflow are rapidly becoming students' preferred math references. The Polymath blog organizes massive mathematical collaborations. Other blogs organize previously isolated researchers into new fields of research. The slow, methodical deliberations of referees in the old school are giving way; now in a single stroke, Tao blogs, gets feedback, and publishes.
Machine Learning is in its ascendancy. LogAnswer and Wolfram Alpha answer our elementary questions about the quantitative world; Watson our Jeopardy questions. Google Page ranks our searches by calculating the largest eigenvalue of the largest matrix the world has ever known. Deep Blue plays our chess games. The million-dollar-prize-winning Pragmatic Chaos algorithm enhances our Netflix searches. The major proof assistants now contain tens of thousands of formal proofs that are being mined for hints about how to prove the next generation of theorems.
Mathematical models and algorithms rule the quantitative world. Without applied mathematics, we would be bereft of Shor's factorization algorithm for quantum computers, Yang-Mills theories of strong interactions in physics, invisibility cloaks, Radon transforms for medical imaging, models of epidemiology, risk analysis in insurance, stochastic pricing models of financial derivatives, RSA encryption of sensitive data, Navier-Stokes modeling of fluids, and models of climate change. Without it, entire fields of engineering from Control Engineering to Operations Research would close their doors. The early icon of mathematical computing, Von Neumann, divided his final years between meteorology and hydrogen bomb calculations. Today, applications fuel the economy: in 2011 rankings, the first five of the "10 best jobs" are math or computer related: software engineer, mathematician, actuary, statistician, and computer systems analyst [CC111].
Computers have rapidly become so pervasive in mathematics that future generations may look back to this day as a golden dawn. A comprehensive survey is out of the question. It would almost be like asking for a summary of applications of symmetry to mathematics. Computability - like symmetry - is a wonderful structural property that some mathematical objects possess that makes answers flow more readily wherever it is found.
It has become common for problems in mathematics to be first verified by computer and later confirmed without them. Some examples are the construction of sporadic groups, counterexamples to a conjecture of Euler, the proof of the Catalan conjecture, and the discovery of a formula for the binary digits of π.
Perhaps the best known example is the construction of sporadic groups as part of the monumental classification of finite simple groups. The sporadic groups are the 26 finite simple groups that do not fall into natural infinite families. For example, Lyons 1972) predicted the existence of a sporadic group of order
2 8 · 3 7 · 5 6 · 7 · 11 · 31 · 37 · 67.
In 1973, Sims proved the existence of this group in a long unpublished manuscript that relied on many specialized computer programs. By 1999 , the calculations had become standardized in group theory packages, such as GAP and Magma [HS99]. Eventually, computer-free existence and uniqueness proofs were found [MC02], [AS92].
Euler conjectured (1769) that a fourth power cannot be the sum of three positive fourth powers, that a fifth power cannot be the sum of four positive fifth powers, and so forth. In 1966, a computer search [LP66] on a CDC 6600 mainframe uncovered a counterexample:
27^5 + 84^5 + 110^5 + 133^5 = 144^5 ,
which can be checked by hand (I dare you). The two-sentence announcement of this counterexample qualifies as one of the shortest mathematical publications of all times.
The Catalan conjecture (1844) asserts that the only solution to the equation
x^m − y^n = 1,
in positive integers x, y, m, n with exponents m, n greater than 1 is the obvious
3^2 − 2^3 = 1.
That is, 8 and 9 are the only consecutive positive perfect powers. By the late 1970s, Baker's methods in Diophantine analysis had reduced the problem to an astronomically large and hopelessly infeasible finite computer search. Mih ̆ailescu's proof (2002) of the Catalan conjecture made light use of computers (a one-minute calculation), and later the computer calculations were entirely eliminated [Mih04], [Met03].
Bailey, Borwein, and Plouffe found an algorithm for calculating the nth binary digit of π directly: it jumps straight to the nth digit without first calculating any of the earlier digits. They understood that to design such an algorithm, they would need an infinite series for π in which powers of 2 controlled the denominators. They did not know of any such formula, and made a computer search (using the PSLQ lattice reduction algorithm) for any series of the desired form. Their search unearthed a numerical identity
! ! n ∞ X 2 1 1 1 4 − − − , π = 8n + 1 8n + 4 8n + 5 8n + 6 16 n=0
which was then rigorously proved and used to implement their binary-digits algorithm.
until recently, no arrangements of regular tetrahedra with high density were known to exist. In 2000, Betke and Henk developed an efficient computer algorithm to find the densest lattice packing of a general convex body [BH00]. This opened the door to experimentation [CT06]. For example, the algorithm can determine the best lattice packing of the convex hull of the cluster of tetrahedra in Figure 3. In rapid succession came new record-breaking arrangements of tetrahedra, culminating in what is now conjectured to be the best possible [CEG10]. (See Figure 4.) Although Chen had the panache to hand out Dungeons and Dragons tetrahedral dice to the audience for a hands-on modeling session during her thesis defense, the best arrangement7 was found using Monte Carlo experiments. In the numerical simulations, a finite number of tetrahedra are randomly placed in a box of variable shape. The tetrahedra are jiggled as the box slowly shrinks until no further improvement is possible. Now that a precise conjecture has been formulated, the hardest part still remains: to give a proof.
L. Fejes Toth proposed a strategy to prove Kepler's conjecture in the 1950s, and later he suggested that computers might be used. The proof, finally obtained by Ferguson and me in 1998, is one of the most difficult nonlinear optimization problems ever rigorously solved by computer [Hal05b]. The computers calculations originally took about 2000 hours to run on Sparc workstations. Recent simplifications in the proof have reduced the runtime to about 20 hours and have reduced the amount of customized code by a factor of more than 10.
The four-color theorem is the most celebrated computer proof in the history of mathematics.
The conjecture is that every finite projective plane of order n > 1 is a prime power. The smallest integers n > 1 that are not prime powers are
6, 10, 12, 14, 15, . . .
The brute force approach to this conjecture is to eliminate each of these possibilities in turn. The case n = 6 was settled in 1938. Building on a number of theoretical advances [MST73], Lam eliminated the case n = 10 in 1989, in one of the most difficult computer proofs in history [LTS89]. This calculation was executed over a period of years on multiple machines and eventually totaled about 2000 hours of Cray-1A time. Unlike the computer proof of the four-color theorem, the projective plane proof has never received independent verification. Because of the possibilities of programming errors and soft errors (see Section 3.5), Lam is unwilling to call his result a proof. He writes, "From personal experience, it is extremely easy to make programming mistakes. We have taken many precautions, . . . Yet, I want to emphasize that this is only an experimental result and it desperately needs an independent verification, or better still, a theoretical explanation" [Lam91]. Recent speculation at Math Overflow holds that the next case, n = 12, remains solidly out of computational reach [Hor10].
Lorenz conjectured in 1963 that his oscillator has a strange attractor (Figure 7). In 1982, the Lax report cited soliton theory and strange attractors as two prime examples of the "discovery of new phenomena through numerical experimentation," and calls such discovery perhaps the most "significant application of scientific computing" [Lax82]. Smale, in his list of 18 "Mathematical Problems for the Next Century" made the fourteenth problem to present a rigorous proof that the dynamics of the Lorenz oscillator is a strange attractor [Sma98] with various additional properties that make it a "geometric Lorenz attractor."
Tucker has solved Smale's fourteenth problem by computer [Tuc02] [Ste00]. One particularly noteworthy aspect of this work is that chaotic systems, by their very nature, pose particular hardships for rigorous computer analysis. Nevertheless, Tucker implemented the classical Euler method for solving ordinary differential equations with particular care, using interval arithmetic to give mathematically rigorous error bounds. Tucker has been awarded numerous prizes for this work, including the Moore Prize (2002) and the EMS Prize (2004).
Mandelbrot's conjectures in fractal geometry have resulted in two Fields Medals. Here he describes the discovery of the 4/3-conjecture made in [Man82]. "The notion that these conjectures might have been reached by pure thought - with no picture - is simply inconceivable.. . . I had my programmer draw a very big sample [Brownian] motion and proceeded to play with it." He goes on to describe computer experiments that led him to enclose the Brownian motion into black clusters that looked to him like islands with jagged coastlines (Figure 8). "instantly, my long previous experience with the coastlines of actual islands on Earth came handy and made me suspect that the boundary of Brownian motion has a fractal dimension equal to 4/3" [Man04]. This conjecture, which Mandelbrot's trained eye spotted in an instant, took 18 years to prove [LSW01].
Smale (1958) proved that it is possible to turn a sphere inside out without introducing any creases. 2 For a long time, this paradoxical result defied the intuition of experts...The computer videos of this theorem are spectacular. Watch them on YouTube! As we watch the sphere turn inside out, our intuition grows. The computer calculations behind the animations of the first video (the Optiverse) start with a sphere, half inverted and half right-side out [SFL]. From halfway position, the path of steepest descent of an energy functional is used to calculate the unfolding in both directions to the round spheres, with one fully inverted (Figure 9). The second video is based on Thurston's "corrugations" [LMM94]. As the name suggests, this sphere eversion has undulating ruffles that dance like a jellyfish, but avoids sharp creases. Through computers, understanding.
Weber and Wolf [WW11] report that the use of computer visualization has become "commonplace" in minimal surface research, "a conversation between visual aspects of the minimal surfaces and advancing theory, each supporting the other." This started when computer illustrations of the Costa surface (a particular minimal surface, Figure 10) in the 1980s revealed dihedral symmetries of the surface that were not seen directly from its defining equations. The observation of symmetry turned out to be the key to the proof that the Costa surface is an embedding. The symmetries further led to a conjecture and then proof of the existence of other minimal surfaces of higher genus with similar dihedral symmetries. As Hoffman wrote about his discoveries, "The images produced along the way were the objects that we used to make discoveries. They are an integral part of the process of doing mathematics, not just a way to convey a discovery made without their use" [Hof87].
As explained above, six is the kissing number in two dimensions, 240 is the kissing number in eight dimensions. In three dimensions, the kissing number is 12. This three-dimensional problem goes back to a discussion between Newton and Gregory in 1694, but was not settled until the 1950s. A recent computer proof makes an exhaustive search through nearly 100 million combinatorial possibilities to determine exactly how much the twelve spheres must shrink to accommodate a thirteenth [MT10]. Bachoc and Vallentin were recently awarded the SIAG/Optimization prize for their use of semi-definite programming algorithms to establish new proofs of the kissing number in dimensions 3, 4, 8 and new bounds on the kissing number in various other dimensions [BV08].
At the close of this first section, we confess that a survey of mathematics in the age of the Turing machine is a reckless undertaking, particularly if it almost completely neglects software products and essential mathematical algorithms - the Euclidean algorithm, Newton's method, Gaussian elimination, fast Fourier transform, simplex algorithm, sorting, Sch ̈onhage-Strassen, and many more.
Year Theorem Proof System Formalizer Traditional Proof
1986 First Incompleteness Shankar Goedel
1990 Quadratic Reciprocity Russinoff Eisenstein
1996 Fundamental - of Calculus Harrison Henstock
2000 Fundamental - of Algebra Milewski Brynski
2000 Fundamental - of Algebra Geuvers et al Kneser
2004 Four Color Gonthier Robertson et al.
2004 Prime Number Avigad et al. Selberg-Erd ̈os
2005 Jordan Curve Hales Thomassen
2005 Brouwer Fixed Point Harrison Kuhn
2006 Flyspeck I Bauer-Nipkow Hales
2007 Cauchy Residue Harrison classical
2008 Prime Number Harrison analytic proof
2012 Odd Order Theorem Gonthier Feit-Thompson
Writing about first-order automated reasoning, Huet and Paulin-Mohring [BC04] describe the situation in the early 1970s as a "catastrophic state of the art." "The standard mode of use was to enter a conjecture and wait for the computer's memory to exhaust its capacity. Answers were obtained only in exceptionally trivial cases." They go on to describe numerous developments (Knuth-Bendix, LISP, rewriting technologies, LCF, ML, Martin-L ̈of type theory, NuPrl, Curry-Howard correspondence, dependent types, etc.) that led up to the Coq proof assistant. These developments led away from first-order theorem proving with its "thousands of unreadable logical consequences" to a highly structured approach to theorem proving in Coq.
First-order theorem proving has developed significantly over the years into sophisticated software products. They are no longer limited to "exceptionally limited cases." Many different software products compete in an annual competition (CASC), to see which can solve difficult first-order problems the fastest. The LTB (large theory batch) division of the competition includes problems with thousands of axioms [PSST08]. Significantly, this is the same order of magnitude as the total number of theorems in a proof assistant. What this means is that a first-order theorem provers have reached the stage of development that they might be able to give fully automated proofs of new theorems in a proof assistant, working from the full library of previously proved theorems. sledgehammer. The Sledgehammer tactic is Paulson's implementation of this idea of full automation in the Isabelle/HOL proof assistant [Pau10]. As the name 'Sledgehammer' suggests, the tactic is all-purpose and powerful, but demolishes all higher mathematical structure, treating every goal as a massive unstructured problem in first-order logic. If L is the set of all theorems in the Isabelle/HOL library, and g is a goal, it would be possible to hand off the problem L =⇒ g to a first-order theorem prover. However, success rates are dramatically improved, when the theorems in L are first assessed by heuristic rules for their likely relevance for the goal g, in a process called relevance filtering. This filtering is used to reduce L to an axiom set L 0 of a few hundred theorems that are deemed most likely to prove g.
The problem L 0 =⇒ g is stripped of type information, converted to a first-order, and fed to first-order theorem provers. Experiments indicate that it is more effective to feed a problem in parallel into multiple first-order provers for a five-second burst than to hand the problem to the best prover (Vampire) for a prolonged attack [Pau10], [BN10]. When luck runs in your favor, one of the first-order theorem provers finds a proof. The reconstruction of a formal proof from a first-order proof can encounter hurdles. For one thing, when type information is stripped from the problem (which is done to improve performance), soundness is lost. "In unpublished work by Urban, MaLARea [a machine learning program for relevance ranking] easily proved the full Sledgehammer test suite by identifying an inconsistency in the translated lemma library; once MaLARea had found the inconsistency in one proof, it easily found it in all the others" [Pau10], [Urb07]
...B ̈ohme and Nipkow took 1240 proof goals that appear in several diverse theories of the Isabelle/HOL system and ran sledgehammer on all of them [BN10]. The results are astounding. The success rate (of obtaining fully reconstructed formal proofs) when three different first-order provers run for two-minutes each was 48%. The proofs of these same goals by hand might represent years of human labor, now fully automated through a single new tool. Sledgehammer has led to a new style of theorem proving, in which the user is primarily responsible for stating the goals. In the final proof script, there is no explicit mention of sledgehammer. Metis proves the goals, with sledgehammer operating silently in the background to feed metis with whatever theorems it needs. For example, a typical proof script might contain lines such as [Pau10] hence "x ⊆ space M" by (metis sets into space lambda system sets)
The first line is the goal that the user types. The second line has been automatically inserted into the proof script by the system, with the relevant theorems sets, into etc. selected by Sledgehammer.
The Feit-Thompson theorem, or odd-order theorem, is one of the most significant theorems of the twentieth century. (For his work, Thompson was awarded the three highest honors in the mathematical world: the Fields Medal, the Abel Prize, and the Wolf Prize.) The Feit-Thompson theorem states that every finite simple group has even order, except for cyclic groups of prime order. The proof, which runs about 250 pages, is extremely technical. The Feit-Thompson theorem launched the endeavor to classify all finite simple groups, a monumental undertaking that consumed an entire generation of group theorists.
Gonthier's team has formalized the proof of the Feit-Thompson theorem [Gon12]. To me as a mathematician, nothing else that has been done by the formal proof community compares in splendor to the formalization of this theorem.
To explain the concept of separation of concerns, Dijkstra tells the story of an old initiative to create a new programming language that failed miserably because the designers felt that the new language had to look just like FORTRAN to gain broad acceptance. "The proper technique is clearly to postpone the concerns for general acceptance until you have reached a result of such a quality that it deserves acceptance" [Dij82].
For a long time, proof formalization technology was unable to advance beyond the mathematics of the 19th century, picking classical gems such as the Jordan curve theorem, the prime number theorem, or Dirichlet's theorem on primes in arithmetic progressions. With the Feit-Thompson theorem, formalization has risen to a new level, by taking on the work of a Fields medalist.
At this level, there is an abundant supply of mathematical theorems to choose from. A Dutch research agenda lists the formalization of Fermat's Last Theorem as the first in a list of "Ten Challenging Research Problems for Computer Science" [Ber05]. Hesselink predicts that this one formalization project alone will take about "fifty years, with a very wide margin." Small pieces of the proof of Fermat, such as class field theory, the Langlands-Tunnell theorem, or the arithmetic theory of elliptic curves would be a fitting starting point. The aim is to develop technologies until formal verification of theorems becomes routine at the level of Atiyah-Singer index theorem, Perelman's proof of the Poincar ́e conjecture, the Green-Tao theorem on primes in arithmetic progression, or Ngˆo's proof of the fundamental lemma.
Why use computers to verify mathematics? The simple answer is that carefully implemented proof checkers make fewer errors than mathematicians (except J.-P. Serre). Incorrect proofs of correct statements are so abundant that they are impossible to catalogue. Ralph Boas, former executive editor of Math Reviews, once remarked that proofs are wrong "half the time" [Aus08]. Kempe's claimed proof of the four-color theorem stood for more than a decade before Heawood refuted it [Mac01, p. 115]. "More than a thousand false proofs [of Fermat's Last Theorem] were published between 1908 and 1912 alone" [Cor10]. Many published theorems are like the hanging chad ballots of the 2000 U.S. presidential election, with scrawls too ambivalent for a clear yea or nay. One mathematician even proposed to me that a new journal is needed that unlike the others only publishes reliable results. Euclid gave us a method, but even he erred in the proof of the very first proposition of the Elements when he assumed without proof that two circles, each passing through the other's center, must intersect. The concept that is needed to repair the gap in Euclid's reasoning is an intermediate value theorem. This defect was not remedied until Hilbert's 'Foundations of Geometry.' Examples of widely accepted proofs of false or unprovable statements show that our methods of proof-checking are far from perfect. Lagrange thought he had a proof of the parallel postulate, but had enough doubt in his argument to withhold it from publication. In some cases, entire schools have become sloppy, such as the Italian school of algebraic geometry or real analysis before the revolution in rigor towards the end of the nineteenth century. Plemelj's 1908 accepted solution to Hilbert's 21st problem on the monodromy of linear differential equations was refuted in 1989 by Bolibruch. Auslander gives the example of a theorem 12 published by Waraskiewicz in 1937, generalized by Choquet in 1944, then refuted with a counterexample by Bing in 1948 [Aus08]. Another example is the approximation problem for Sobolev maps between two manifolds [Bet91], which contains a faulty proof of an incorrect statement. The corrected theorem appears in [HL03]. Such examples are so plentiful that a Wiki page has been set up to classify them, with references to longer discussions at Math Overflow [Wik11], [Ove09], [Ove10].
Theorems that are calculations or enumerations are especially prone to error. Feynman laments, "I don't notice in the morass of things that something, a little limit or sign, goes wrong.. . . I have mathematically proven to myself so many things that aren't true" [Fey00, p. 885]. Elsewhere, Feynman describes two teams of physicists who carried out a two-year calculation of the electron magnetic moment and independently arrived at the same predicted value. When experiment disagreed with prediction, the discrepancy was eventually traced to an arithmetic error made by the physicists, whose calculations were not so independent as originally believed [Fey85, p. 117]. Pontryagin and Rokhlin erred in computing stable homotopy groups of spheres. Little's tables of knots from 1885 contains duplicate entries that went undetected until 1974. In enumerative geometry, in 1848, Steiner counted 7776 plane conics tangent to 5 general plane conics, when there are actually only 3264. One of the most persistent blunders in the history of mathematics has been the misclassification (or misdefinition) of convex Archimedean polyhedra. Time and again, the pseudo rhombic cuboctahedron has been overlooked or illogically excluded from the classification (Figure 21) [Gr ̈u11].
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 FIT}{1Mbit} * 64GB * 77 hours = \frac{10^3 errors}{10^9 hours Mbit} * (64 * 8 * 10^3 Mbit) * 77 hours ≈ 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."
This makes perhaps the third instance I've seen today of Amara's law: formal proofs, neural networks (http://www.wired.com/2014/08/deep-learning-yann-lecun/), and paperless offices (http://crookedtimber.org/2014/08/13/origami/).
Mathematics in the Age of the Turing Machine
The article gives a survey of mathematical proofs that rely on computer calculations and formal proofs.
Link: http://arxiv.org/abs/1302.2898
The article gives a survey of mathematical proofs that rely on computer calculations and formal proofs.
Link: http://arxiv.org/abs/1302.2898