Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

In this chapter we revisit computer assisted proofs, which serves to more conclusively illustrate performative and adaptive experiences, and also the limitations of a property-based model of preference evolution, and the capacity of the aesthetic as process theory to satisfactorily deal with a wide spectrum of mathematical aesthetic judgements—including negative ones. In this chapter I utilize much of the discussion advanced in Chaps. 3 and 4, thus, this chapter can be seen as a sort of refinement and closure of that discussion.

As we have seen, Appel and Haken’s computer-assisted proof of the four colour theorem provides us with a conspicuous and interesting case of mathematical ugliness. As Paul Nahin remarks, this proof “is almost always what mathematicians think of when asked ‘What is an example of ugly mathematics?’ ” [69, p. 5]. Although the four-colour theorem itself ranks number nine in David Wells’ list of the most beautiful theorems [94], its computer-assisted proof has been poorly welcomed. But McAllister [64] conjectures that aesthetic induction might eventually alter this negative reception. After all, McAllister argues, aesthetic standards in mathematics seem to depend on the acceptability of the proofs, just as scientific beauty depends on the empirical adequacy of the theories. In Chap. 3 we saw that changes in preferences for certain properties are insufficient to explain ugliness in computer-assisted proofs. We are now in position to better explicate that fact.

1 The Proof

The following is the original introduction of the proof presented in 1976 by Appel and Haken [4]:

The following theorem is proved.

Theorem.

Every planar map can be colored with at most four colors.

As has become standard, the four color map problem will be considered in the dual sense as the problem of whether the vertices of every planar graph (without loops) can be colored with at most four colors in such a way that no pair of vertices which lie on a common edge have the same color. The restriction to triangulations with all vertices of degree at least five is a consequence of the work of A. B. Kempe. Over the past 100 years, a number of authors including A. B. Kempe, G. D. Birkhoff, and H. Heesch have developed a theory of reducibility to attack the problem. Simultaneously, a theory of unavoidable sets has been developed and the fusion of these has led to the proof.

A configuration is a subgraph of a planar triangulation consisting of a circuit (called the ring) and its interior. A configuration is called reducible if it can be shown by certain standard methods that it cannot be immersed in a minimal counterexample to the four color conjecture. […] A set of configurations is called unavoidable if every planar triangulation contains some member of the set. From the definitions, it is immediate that the four color theorem is proved if an unavoidable set of reducible configurations is provided.

The most efficient known method of producing unavoidable sets of configurations is called the method of discharging. This method treats the planar triangulation as an electrical network with charge assigned to the vertices. Euler’s formula is used to show that the initial charge distribution, giving positive charge to vertices of degree five and negative charge to vertices of degree greater than six, has positive total charge […]

Appel and Haken report that by studying different discharge algorithms, with the help of computer programs, they were able to choose an algorithm that produced a set of fewer than 2,000 configurations (let us assume 2,000, for the sake of brevity); each configuration was proved, with the assistance of a computer program, to be reducible. That is, the theorem was proved by dividing the proof into 2,000 cases.

The proof is an instance of proof by cases, in which one analyses, documents, and proves every instance of an assertion in a case-by-case fashion. Proofs by cases are often qualified as cumbersome, clumsy, inelegant, and ugly. Proofs by cases contrast with elegant, parsimonious proofs, such as Cantor’s diagonal method. A multiplicity of cases means lack of simplicity and lack of unity. Despite this fact, the analysis of the experience of a proof by cases is analogous to the analysis of Cantor’s proof: the phenomenological space has simplicity and step-parsimony as dimensions, since these are the relevant properties involved in eliciting an affective response. The difference is that proofs by cases have negative scores on simplicity and parsimony.

Proof by cases can be interpreted as a series of steps, with the peculiarity that each case of the proof is independent of the others and thus each case requires its own proof. This means that there is no narrative connection between cases; rather, each case is an independent story. A proof by cases, as an intentional object, consists of multiple disconnected experiences, each with its own series of steps. A computer-assisted proof further worsens this scenario, since the proof itself only offers a general description of the cases to prove, and we have to trust that the computer has documented the truth of each case. As we saw in Chap. 3, this means that the computer-assisted proof does not even offer a complete intentional object on which we can focus our attention. To see this clearly, let us analyse the experience in more detail.

2 Experience

Our aesthetic-process begins by focusing our attention on the four colour theorem, and, more importantly, on its proof. Before we can appreciate the theorem or the proof we must be able to see them. Background understanding is necessary. Let us assume that the appropriate background is graph theory, (GT). Our phenomenological space has GT as a dimension, defined as follows:

$$\displaystyle{\mathit{GT = thefeatureofbeingunderstandableonlyifgraphtheoryhasbeenunderstood}}$$

With this background we actively follow the introductory reasoning presented by the authors, in a fashion similar to a step-series interpretation of the proof. Each step becomes an object of attention. We perform certain activities; we check for logical story development to accept the next step. We eventually arrive at the 2,000 maps to be discharged. These maps constitute the cases necessary to prove the theorem. At this point, a regular proof would involve another 2,000 small proofs. But the authors tell us only that every case was checked by means of a computer. This is peculiar, since this step does not allow us to focus our attention actively—which is characteristic of proofs as intentional objects. Rather, it offers only the passive acceptance of the computer’s results. The proof offers only black-box outputs, so to speak.

Now, in Chap. 3 we saw that methodological and epistemological concerns about computer-assisted proofs do not play a significant role in their aesthetic evaluation. Let us assume that the proof is epistemic and methodologically sound. Even so, our experience of the 2,000 steps of the proof is that of mere acceptance of the results. In these last 2,000 steps we are not even offered a passive object of attention. Our experience is occurring in a space whose first dimension is background understanding; but a result from a computer does not need any special understanding: we only need to accept it. The nature of the results generated by a computer does not allow us to interpret them as intentional objects in our phenomenological space. Unlike the steps of a regular proof, the results of computer programs do not require neither the background understanding nor the active attention characteristic of experiences of proofs. The steps do not play the role of engaging us in intellectual activity to elicit pleasure. Now, this fact does not turn our experience into a negative experience; it turns it into an incomplete experience.

We can rephrase our conclusion in Chap. 3. Mathematicians do not appreciate computer-assisted proofs simply because they do not offer anything (or they offer very little) to be appreciated: even if we know and understand the kind of operation the computer performs, we cannot actually have the experience of following the last 2,000 steps of the proof; we do not perform any intellectual activities ourselves and we do not even have an object to passively appreciate.

Now, one might argue that, in principle, we know the kind of operations and processes a computer performs. This knowledge can be the basis of an experience in the same way graph theory is. But the introduction of knowledge of computer programming is still a problem for two reasons. First, the knowledge involved in knowing what the program does is different from our background understanding. This knowledge is about the working principles of computers, or about programming principles, or even about the exact computer code employed. But it is not our background understanding knowledge GT. There is still a kind of interruption of our original mathematical experience. We suddenly jump in the middle of our proof from our GT phenomenological space to another, computer-programming space. Second, mathematicians do not see themselves as computer programmers, code writers or debuggers. By introducing computer-programming events, mathematicians, in a sense, are forced into alien territory. It is true that all these activities can be seen as beautiful, but it would be a different kind of beauty; computer-programming beauty. Computer-programming beauty may have its own principles and types of experience in a manner similar to how mathematical beauty has its types of experience and principles; but it is still an alien kind of beauty in relation to our original mathematical beauty. When we suddenly introduce computer-related knowledge in the midst of a traditional mathematical argument we interrupt the original experience and switch to an experience of computer-programming items. Although this is not the same as an incomplete experience, my argument still holds, since the interruption turns the original experience into something else. The introduction of computer-programming events as the focus of attention alienates our mathematical experience. The cases of an incomplete experience and a switch of attention to a computer-programming item experience (we can call it an alienated experience) can be understood in similar terms: in both cases we are not provided with experiences that are characteristically mathematical.

In the computer-assisted proof of the four colour theorem the content of the experience is similar to a proof by cases, except for the last 2,000 steps, which are absent from our experience. Our experience of the proof is similar to the experience we would have if someone told us a story that resulted in 2,000 other stories, except the author would not tell us those 2,000 stories; rather, he would ask us to accept that all those stories have happy endings; resulting in a feeling of frustration. Let us recall that not only contemplating properties, but also performing mental activities elicits affective responses. The feeling of frustration does not come from the properties of the proof, but, analogously to Cantor’s diagonal, from the outcome of our activities. In summary, the content of experience can be interpreted as an intentional object similar to the aesthetic mathematical intentional object of a proof by cases, except for the fact that the last steps are missing: our intentional object is a crippled, deformed intentional object, and the affective response of displeasure is due to the unsatisfactory way the story’s conclusion is reached. Since we have an incomplete object of attention, it is not likely that the passive content of the experience elicits an affective response, so the response of frustration, caused by the active content, plays the most significant role. The output of the pleasure-relation for this proof can be expressed as:

$$\displaystyle{f(\mathit{semi - AMIO - 4colour,incompleteactivities}) = (N,D)}$$

3 Value

In Chaps. 3 and 4 we saw that in McAllister’s conception of the aesthetic induction it makes sense to conjecture that computer-assisted proofs might one day be regarded as beautiful, as their acceptance grows. However, in Chaps. 4 and 5, the constrained model of aesthetic induction rendered a different result. As in the case of Cantor’s proof, in addition to aesthetic induction, an aesthetic experience can be enhanced by a change in the constitution of the experience. Thus, in our model, we have two possible scenarios for a change in the aesthetic value of computer-assisted proofs: by constrained aesthetic induction and by change in experience. Let us analyse these two scenarios.

3.1 Scenario 1: Change by Aesthetic Induction

Let us assume that the acceptance of computer-assisted proofs grows. Mathematicians no longer argue about the soundness of the results generated by computers and are not concerned about any of their epistemic or methodological drawbacks. Our proof of the four-colour theorem would be just a perfectly valid proof by cases. However, as we discussed in Chap. 4, proofs by cases have been regarded as a good and acceptable method since they first appeared, and the method is as old as mathematics itself. There has never been shortage of proofs by cases and every mathematician is very familiar with the method. But this familiarity has not resulted in an increase in mathematician’s preference for proofs by cases. It seems thus that the properties associated with proofs by cases exhibit negative robustness: their appreciation tends to stay negative. The set of properties associated with proofs by cases (lack of simplicity, lack of parsimony) exhibits low or negative critical adequacy and a high degree of robustness. All the evidence shows that the method’s value is not likely to change. Proofs by cases are not aesthetically appreciated, and that fact seems to remain stable. Now, the assistance of computers does not entail anything that may affect those traits in any relevant way. We thus have reasons to think that proofs by cases shall remain negatively judged, since it seems implausible that, one day, computer-assisted proofs by cases would be judged positively, despite the fact that regular proofs by cases were judged negatively.

3.2 Scenario 2: Change in the Nature of Our Experience

We can once again draw an analogy with our discussion of the diagonal method, where we established that our first experience of the proof is different from ulterior experiences, in which we become aware of the method’s unification power. Once the diagonal method has become widely applicable, the property of method-unification plays a significant role in enhancing our appreciation. Let us assume that something similar occurs to computer-assisted proofs; they become so powerful and acceptable that they begin to appear in different kinds of proofs. The constitution of the experience changes; the content of our aesthetic experience is no longer the original content associated with our first computer-assisted proof by cases of the four-colour theorem. We now have a new property to consider, method-unification, which may result in improving our judgement of computer-assisted proofs in general. However, the assistance of the computer remains in all instances of experiences of computer-assisted proofs. This means that at least one part of the proof consists in accepting results generated by the computer. This acceptance of the results cannot result in an intentional object (or at least in a non-alienated object), and it also prevents us from performing any (non-alienated) activities in that specific step. This is analogous to having many different ways of telling stories, all of them sharing the feature that at some point we are asked to pretend that an event convenient for concluding the story just happened.

Even if the computer-assisted-proof method is ubiquitous and method-unification is important, it remains the case that our experience’s content is an incomplete content (or an alienated content), for that is the very nature of accepting results from a computer: the computer-assisted steps translate into circumventing experience steps (or into shifting to a computer-programming experience): accepting results is equivalent to bypassing mathematical experience.

The problem with computer-assisted proofs is not acceptability (as it is in the case of aesthetic induction), but rather that the computer-assisted steps of the proof only give us something to accept and not something to appreciate (at least, not without alienating our mathematical experience). Acceptability can be settled by addressing the relevant epistemic issues of the assistance of computers. If I were trying to establish the validity of a certain theorem, accepting a result is correct as far as there are no epistemic problems with that acceptance. But this acceptance still does not give us something to appreciate (that is, something to contemplate or some task to perform); and having something to appreciate constitutes the very basis of aesthetic experience. Acceptability is not appreciability. For aesthetic evaluation, having something to see is a precondition, and accepting results is just bypassing this condition. Acceptance does not even need background understanding: we do not need to understand anything in order to accept a result. Accepting results is something very different from experiencing mathematics.

In the experience and enjoyment of doing mathematics, a mathematician becomes engaged in understanding assertions, or in performing intellectual activities. In aesthetic experience this engagement is further deepened by changing the way our attention is focused and by undergoing affective responses. This is what aesthetic experience is; mathematical engagement plus affective engagement. In any aesthetic experience we want to see something, we want to engage in appreciation. But accepting a result is not seeing or doing; it is avoiding experience. If someone covered my eyes in front of a painting and I was not able to see it, I could still believe the painting is there and it has certain characteristics—if, for instance, I accepted the testimony of someone reliable. But if I were asked about my experience of the painting, I would be able to answer only that I have none, because I cannot see the painting. The same occurs with computer-assisted steps of proofs. Even if a property such as method unification is added to the experience, it does not change the crucial fact that the experience still has deforming narrative gaps. A computer-assisted proof shall always give us an incomplete experience, something we cannot fully appreciate, despite the fact that the proof is a perfectly acceptable and widespread method. Thus, it is not very plausible that we shall come to regard computer-assisted proofs as beautiful.