Previous post: Where one can find an autobiography of Alexander Grothendieck? Part 2
A draft of this post was written quite a while ago. It was intended to be an opening of a series of posts. These posts may be written soon, or may never be will be written. Anyhow, I decided to post it "as is". The original title of the post was the following.
"Mathematics is a human activity."
This used to be such a platitude that hardly anybody dared to write it down, at least is such a straightforward form. This is not the case anymore. Some of the most prominent mathematicians do no share this position, including two Fields medalists. Timothy Gowers advocates a program of replacing mathematicians by computers. Vladimir Voevodsky quit algebraic geometry and algebraic K-theory, at least for the time being, and working on a program of computer verification of proof. Admittedly, his goals are more modest: computer verification of proofs; finding proofs is still left to humans.
A highly publicized example is the claim that Thomas Hales proved the so-called Kepler’s conjecture. The “proof” depends on verification of a huge number of statements by computers. His proof is almost accepted. Apparently, the experts are not quite satisfied even with the part of his proof he wrote for humans. Being not satisfied by such an “almost acceptance”, he decided to produce a new proof. But he has no intention to present a proof which his fellow mathematicians will be able to comprehend to their satisfaction. He is guiding a big project which, he expects, will lead to a proof of Kepler’s conjecture verifiable by computers from the first principles. In other words, his answer to the difficulties of his fellow mathematicians in reading his article (published in “Annals of Mathematics” with a special preface by the editors) is to make the whole argument inaccessible to humans.
Of course, the computer-assisted solution of the 4-colors problem by K. Appel and W. Haken is well known even to the general public. This computer-assisted proof is old enough to judge its usefulness for mathematics. It eliminated a stimulating problem in the graph theory, and did not lead to any progress on related conjectures such as the Hadwiger conjecture, for example. Since the claimed theorem itself is useless even within the pure mathematics, the total impact is negative.
All these mathematicians are missing the main point: mathematics is a human activity. They miss it notwithstanding the fact that they themselves are humans, and experience feelings similar to humans working in less esoteric fields.
Voevodsky is the most open about his motives: he was frustrated by the difficulties he experienced in writing down his proof of the Bloch-Kato conjecture and even in convincing himself that his proof is correct. In the end, he convinced both himself and the others, but decided to look for a less painful way to justify his claims. Knowing him to some extent personally, I believe that the fact these claims are his claims is important for him. He would not care much about claims that a computer proved this or that. And this may be the reason why his program seems to be the most meaningful one.
I risk to suggest that both Th. Hales and W. Haken (the driving force of the Haken – Appel team) are (were) motivated by their quest for “immortality” in the sense of the novel “Immortality” by Milan Kundera. To put it simple, by the desire to be remembered as the ones who solved a famous problem, or, at least, a problem as famous as possible.
W. Haken devoted years to attempts to prove the Poincaré conjecture before turning his attention to the 4-colors problem. K. Appel was a computer scientist and, most likely, had a different motivation.
I do not think that a quest for this sort of immortality is a bad thing per se. But when it hurts somebody or something I am attached a lot, as I am attached to mathematics, I dare to disapprove.
Timothy Gowers remains a mystery. As he wrote, he is glad that the humans will not be replaced by computers during his lifetime, but hopes that humans will be eliminated from mathematics in few decades.
Next post: Self-revealing truths?