Four color problem, odd Goldbach conjecture, and the curse of computing

For over twenty-three hundred years, at least since the publication of Euclid’s Elements, the conjecture and proof of new theorems has been the sine qua non of mathematics. The method of proof is at “the heart of mathematics, the royal road to creating analytical tools and catalyzing growth” (Rav, 1999; pg 6). Proofs are not mere justifications for theorems; they are the foundations and vessels of mathematical knowledge. Contrary to popular conception, proofs are used for more than supporting new results. Proofs are the results, they are the carriers of mathematical methods, technical tricks, and cross-disciplinary connections.

Of course, at its most basic level, a proof convinces us of the validity of a given theorem. The dramatic decisiveness of proofs with respect to theorems is one of the key characteristics that set mathematics apart from other disciplines. A mathematical proof is unique in its ability to reveal invalid conclusions as faulty even to the author of that conclusion. Contrast this with Max Planck’s conception of progress in science:

A new scientific truth does not triumph by convincing its opponents and making them see the light, but rather because its opponents eventually die, and a new generation grows up that is familiar with it.

Further, unlike in science, a mathematical conclusion is shown to be faulty by the proofs and derivations of other mathematicians, not by external observations. In fact, if we use Karl Popper’s falsification as the criterion for science then mathematics (as practiced) is clearly distinct. A typical statement, such as the recently proven odd (or, weak) Goldbach conjecture states:

Weak Goldbach conjecture

Every odd integer is the sum of three primes.

Given any specific integer , we can verify that it is the sum of three primes by looking at the finite list of primes less than and seeing if any three of them (with repetitions allowed) add up to . In other words, we could set a computer program running to check odd numbers one at a time, and if we ever came to one that can’t be written as the sum of three primes then we would have falsified (in the proper Popper sense) our conjecture.

“What makes this unscientific?”, you ask, “the weak Goldbach conjecture is precise and falsifiable, Popper would call it science.” The distinction is in how math is practiced, if the weak Goldbach conjecture only had to pass scientific standards of truth then it would have been an accepted result 271 years ago when Christian Goldbach first doodled it in the margins of his letter to Leonhard Euler. We wouldn’t need top mathematicians like H.A. Helfgott proving it.

What the mathematical community needs is a clear argument that shows that the conjecture holds for all odd integers, not just the ones we bothered to test. A poor programmer might jump at this opportunity by (1) writing down a program that looks at the odd integers one at a time and halts only if finds a counterexample. He could then (2) write a second program that takes the code of any program and decides if it will halt or not; maybe if the task proves too difficult, he could offer $1000 for it on GetACoder.com. Finally, (3) if the second program reports that the first program halts then there must be a counterexample and the conjecture is false, and if the second program reports that the first program doesn’t halt then the odd Goldbach conjecture is true.

Of course, you realized that the second step is the Halting problem that Alan Turing famously proved to be undecidable. For computer scientists, in fact, the saddest news in the resolution of the odd Goldbach conjecture is that they can no longer use it as an example when introducing the Halting problem in COMP-101. However, as theorists, we can suspend our disbelief and pretend that maybe we could solve the Halting problem, what would that mean for mathematics?

If we simply had a mechanical oracle like Rav’s PYTHIAGORA that can read any conjecture and definitely declare if it is valid or not and “if all our toil and sweat in proving theorems served only to ascertain whether they were true or not, then PYTHIAGORA would deliver us of useless labors and frustrations” (Rav, 1999; pg. 6). Such a road would not lead us towards a mathematical paradise and Rav shows that if PYTHIAGORA existed then it “would have dealt a death blow to mathematics, for we would cease having ideas and candidates for conjectures” (Rav, 1999; pg. 6). A proof does more than verify a conjecture, it (often) establishes connections between fields, or introduces new methods and questions that are useful beyond the proven theorem. Most importantly, a proof is not a blackbox, it is a narrative to be consumed by the mathematician. What the mathematical community wants is the argument for the odd Goldbach conjecture to be beautiful and insightful, to build understanding.

Although the universal PYTHIAGORA of our imagination is impossible, computer assisted proofs run the risk of moving us closer to this dystopia. Any discussion of computers in mathematics has to open with the four color problem; a problem that began its life in 1852 as a conjecture in graph theory: given any separation of a plane into contiguous regions, are four colors enough to color the regions of the map so that no two regions that share a common boundary (that is not a corner, where corners are the points shared by three or more regions) have the same color? In 1977, Kenneth Appel, Wolfgang Haken, and John Koch published a computer-assisted proof and birthed the new four color problem, a philosophical question about the nature of proof and the role of computers in mathematics. Thomas Tymoczko addressed the new problem in his 1979 paper: “The four-color problem and its philosophical significance”.

Tymoczko (1979) characterizes proofs based on the anthropology, epistemology and logic of mathematics. Proofs are (a) convincing, (b) surveyable, and (c) formalizable. Surveyability plays a key role in Tymoczko’s analysis and he defines a proof as surveyable if it can be looked over and verified by a rational agent under realistic constraints. Without surveyability, a proof is not a priori.

In the four-color theorem (4CT), a key lemma was obtained by a computer. Appel and Haken provided an inductive proof for the 4CT, which relies on considering the reducibility of 1834 configurations. Note that unlike the poor programmer’s approach to the odd Goldbach conjecture, real math is involved in first reducing the infinite number of possible partitions of the plane into a finite number of restricting configurations. Establishing the reducibility of each configuration is tedious and long, but algorithmic. Koch provided the algorithm for verifying the reducibility of the configurations and the verification by computer serves as the lemma which completes the proof by induction.

Yesterday’s proof of the odd Goldbach conjecture by Harald Andrés Helfgott (2012,2013) follows a similar pattern of reducing an infinite statement to a proof with a large and finte number of casses to verify by computer. Helfgott applies the circle method that was developed by Hardy and Ramanujan in 1916. The method usually produces statements of the form ‘for sufficiently large (i.e. ) such-and-such property holds’. Helfgott refined the method to have ‘such-and-such property’ mean ‘is a sum of 3 primes’, and tightened to be about . This application of circle method was the math of the proof, and a computer search was used to manually establishing a lemma for .

The brute-force proof of this computer lemma is so long that no mathematician has, or even can, survey the proof; thus, Tymoczko (1979) argues, mathematicians must trust the accuracy of their computers – an experiment! If mathematicians are to accept the 4CT they must acknowledge the lemma as a computer experiment, much like ones in natural sciences. For Tymoczko (1979), this distinction for computer assisted proofs makes them a posteriori and leads down a road of quasi-empiricism.

From my experience as a programmer and the difficulty of ensuring that code is accurate, I agree that assistance from a computer can sometimes feel like an experiment. However, Gontheir (2009) formally shown that there are no programming errors in the proof of the 4CT. But that doesn’t make the proof surveyable in Tymoczko’s sense; at least not by a human, only by the rational agency of a computer. But this is not unique to computer assisted proofs, most modern mathematical proofs are so extensive that many of them are not surveyable from first principles; the proofs rely on previous theorems and results. For many modern proofs, a single mathematician has no chance of surveying the whole proof and all the previous results it is based upon (and the results those results are based on, etc.). Mathematicians rely on modularity; they take previously proven statements as true and seldom question their validity. So surveying a proof is simply looking at the novel material and taking previous results as given, therefore a proof is surveyable not if a single rational agent can survey it, but if a collection of agents can do it. With my definition of surveyability that accounts for the modularity of mathematics, surveying the 4CT becomes much more tractable. Even though one mathematician has no chance of surveying all 1834 configurations considered by the computer, she can survey a single configuration and together 1834 mathematicians can survey the 4CT. Thus, I cannot accept Tymoczko’s argument that computer assisted proofs are necessarily a posteriari, but I agree that something smells fishy.

For me, the issue is not general surveyability, but internalization. No mathematician fully understands the computational part of the proof, at least no more than a pointy-haired boss understands the task his engineers completed. Although some AI enthusiasts might argue that the computer understands its part of the proof, most mathematicians (or people in general) would be reluctant to admit computers as full participants in the “social, informal, intuitive, organic, human process” (De Millo, Lipton, & Perlisp, 1979; pg. 269) of mathematics. For De Millo, Lipton, & Perlisp (1979), PYTHIAGORA’s verification or the computer assisted part of a proof is simply meaningless; it does not contribute to the community’s understanding of mathematics. This is easiest to see in the odd Goldbach conjecture: what understanding do we gain from the odd numbers that Helfgott’s computer program checked? It teaches us no new mathematics, no new methods, and brings no extra understanding beyond a verification.

In an alternative world without computer proofs, this verification would be absent. On the one hand, this means that alternative Helfgott would only tighten but not resolve the conjecture. On the other hand, the problem would remain open and continue to keep researchers motivated to find completely analytic ways to resolve it. Of course, even in our real world, a few mathematicians will continue looking for a non-computer assisted proof of the weak Goldbach conjecture, just as they continue to do with the four color theorem. However, the social motivation will be lower and progress slower. This is the curse of computing: giving up understanding for an easy verification.

Of course, I don’t mean this to detract from Helfgott’s breakthrough, the real danger of the curse is not among mathematicians but among theorists and modelers. Instead of the mathematical reasoning and deep understanding encouraged by biologists, economists, and physicists of the past, theorists today are increasingly satisfied with computer simulations. In fields where the simulations can be directly linked to experiment (physics, chemistry, etc) this is largely alright. In biology, economics, and the social sciences, however, the link of simulation to experiment is weak or nonexistent. Models serve as heuristics to inform largely verbal theories. They are built to pump out surprising results but not to extend understanding. Ironically, the co-founder of the Santa Fe Institute (the home of agent-based modeling and complexology) Murray Gell-Mann best states the computing dilemma:

What is the point of studying a complex system that we don’t understand by making a computer model that we don’t understand?

My pessimistic answer is ‘it’s easy’, writing an ‘abstract’ simulation is much simpler than trying to pursue an analytic result. If the simulations were actually treated as heuristics and followed up by rigorous treatments then this ease would not be a problem. However, it seems that in some fields simulations are increasingly discouraging follow up work. Once a computational model hints at a previously paradoxical effect, it often spells doom for understanding. Follow up papers that extend beyond number crunching to show general results are faced by the wall of “this isn’t novel” and rejected. The curse of computing is settling for examples or easy verification at the expense of a slower but deeper understanding. As computer scientists start to rewrite their COMP-101 courses to remove the Goldbach conjecture as a motivation for the halting problem, I hope that in its place they will stress replacing heuristic models by rigorous understanding.

References

Appel, K., & Haken, W. (1977). Every planar map is four colorable. Part I. Discharging. Illinois J. Math 21: 429–490.

Appel, K., Haken, W., & Koch, J. (1977). Every planar map is four colorable. Part II. Reducibility. Illinois J. Math 21: 491–567.

Helfgott, H.A. (2012). Minor arcs for Goldbach’s problem. arXiv preprint 1205.5252

Helfgott, H.A. (2013). Major arcs for Goldbach’s problem. arXiv preprint 1305.2897

De Millo, R. A., Lipton, R. J., & Perlis, A. J. (1979). Social processes and proofs of theorems and programs. Communications of the ACM, 22(5), 271-280.

Gonthier, G. (2008). The four colour theorem: Engineering of a formal proof. In Computer Mathematics . Springer Berlin Heidelberg. [preprint version]

Rav, Y. (1999). Why Do We Prove Theorems? Philosophia Mathematica, 7 (1), 5-41 DOI: 10.1093/philmat/7.1.5

Tymoczko, T. (1979). The four-color problem and its philosophical significance. The Journal of Philosophy, 76(2): 57-83.