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

**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.**

*his claims*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?

This comment has been removed by the author.

ReplyDeleteI have always believed and still believe the whole purpose of mathematics and mathematicians is to improve the human understanding of mathematics. And I think this was one of the points of Thurston's famous essay "On Proof and Progress in Mathematics". A proof that can't verified by a human being doesn't really add anything to the human understanding of mathematics. If someone has a proof for something which is too complicated for other mathematicians , I think the next step should find a more conceptual proof which is more easier rather than building computer systems to verify a complicated proof. The best case scenario would be case the theorem with a very complicated proof almost becomes tautology when viewed as part of very some general theory ( "The Rising Tide" of Grothendeick ). And to me that's what the purpose of mathematics should be.

ReplyDeleteAbsolutely.

DeleteThis comment has been removed by the author.

ReplyDelete"Timothy Gowers remains a mystery. As he wrote, he is glad that humans will not be replaced by computers in his lifetime ..." Gowers was born in 1963 C.E. According to the conjecture of Ray Kurzweil, the full onset of the technological singularity will occur by 2045 C.E. This conjecture says that the net AI intelligence (add up the IQs of all the AI entities) will exceed the net human intelligence (add up the IQs of all humans in the solar system) by a factor of at least one billion. I conjecture that Kurzweil is the world's greatest living genius and the world's 3 greatest living scientists are James D. Watson, Sydney Brenner, and M. Milgrom.

ReplyDeleteAlas, you are at the wrong place. Apparently, R. Kurzweil made some important contributions to the modern technology. But this is very far from the issue this blog is devoted to. And his success in selling bad science-fiction by pretending that it is a good science is only one of the many similar examples. Perhaps, it deserves a study as an example of crowd-management technologies.

DeleteOn a technical level, I would like to point out that adding IQs doesn't make any sense, as also the the phrase "net intelligence" of humans, aliens, computers - whatever you like.

Regardless of what the "purpose" of mathematics is, can't we all agree that it is sometimes useful to have a heuristic telling us that something is (or likely to be) true, even if we don't yet understand why?

ReplyDeleteVerification and understanding are both purposes that math papers have been said to serve. I have seen many cases where serving these concerns independently has yielded much better results.

Heuristic telling - sure. On this level we know that the Riemann hypothesis is true, and this is very useful. The point is exactly this: we have a lot of human-understandable heuristic narratives behind this knowledge.

DeleteIndeed, it is often

saidthat one of the purposes of the mathematical papers is the verification. This is even true in a sense: with very rare exceptions, a good mathematician is unable to write down a seriously fallacious argument with details. She or he discovers flaws in the process of writing things down.But I am not aware of any significant mathematical result which was verified separately from understanding. Occasionally, some result is established for all, say, sufficiently big natural numbers. If the bound is explicit and manageable, one can verify the cases of "small" numbers by hand or on a computer. But this is not understanding.

Sometimes it is claimed that we verified a result, but we still do not understand why it is true. I myself made such claims, and may be even published a couple. But this has different meaning: the proof is understood, but the level of understanding appears to be insufficient. We suspect some deeper reason for the result to be true.

I should clarify one point in my reply.

DeleteA brute force verification of "small" cases is acceptable only to the extent we are not particularly interested in these small cases. Such a verification is used mostly to get a nice *statement* of the form "For ALL" things of some sort (say, natural numbers), something nice is true.

But sometimes we are interested, first and foremost, in the small cases. Then we may first verify a result using computers, but then we will look for a human-understandable arguments.

A good example is provided by the theory of simple finite groups. There are so-called exceptional finite simple groups, 26 of them (if we trust experts). Therefore, all sufficiently big simple groups are not exceptional. But is turns out these exceptional groups are extremely interesting and beautiful. Some of them were originally found using computers (first to provide evidence that such interesting gadgets exists, then to verify that they do exist indeed). But in this branch of mathematics computer-independent proofs are valued even if a computer-based proof exists. Moreover, they are valued more, and a problem is not considered solved till it gets a computer-independent solution.

I did not followed this in recent years, so I am not sure that all computer-dependent arguments were eliminated by now. In fact, this field has more pressing problems.

Let me try to dispel the mystery about my views. I share your distaste for incomprehensible proofs that merely certify the truth of a statement without giving us any idea of why it is true. Maybe there are a few results like the four-colour theorem where some kind of gigantic check is necessary; perhaps there is no satisfying reason that the check turns out to work. But that is not the kind of proof that interests me. What I like is characteristically human proofs that really explain to me what is going on.

ReplyDeleteSo where do computers come in? Simply that I believe that computers will one day be able to find these beautiful, humanly satisfying proofs without our help. Furthermore, before that day, I see them playing a greater and greater role in helping mathematicians -- for example, saving us from trying to prove a lemma when there is an easy counterexample that we have missed, or telling us that a statement we are trying to prove closely resembles a result proved in an obscure paper somewhere. This kind of help would cut a lot of the drudgery out of doing research and leave just the interesting part. But it would not be a stable situation, because as the technology improved, the computers would be able to do even the interesting part (including choosing what to work on in a tasteful and characteristically human way) and our role would be reduced to reading and understanding their output.

In short, I imagine a brief golden age of cooperation between humans and computers, followed by computers becoming better mathematicians than we are -- not in the brute-force way that they are better at chess, but in the genuine sense of being able to find proofs that are beautiful and explanatory and to do so much more quickly than we can. And while that would be sad for mathematicians, I do not think it would be sad for humanity as a whole: it would be far from the first time in human history that technological progress has made a whole kind of career redundant.

Dear Sir Timothy,

ReplyDeleteThanks a lot for finally visiting my blog. I also appreciate a lot that you included my blog into the blogroll in your blog.

Thanks for your explanations. I am glad that you are interested in "characteristically human proofs", in contrast with, say Thomas Hales. But this is not a surprise, of course. This is exactly what makes your position so interesting and mysterious. Your comment does not explain this mystery, at least for me.

I was planning to lay down a background for a discussion of your position, but, to my regret, there is too much of quite different sort of "drudgery" in my life, and I only started of writing my ideas down in this post and the next one. Perhaps, a better way to go will be just to write a detailed reply to you. For at least today, or the time being, I have to limit myself by a few remarks. To be continued in the next comment.

Before writing it, I would like to uncover my incognito - if you still don't know my name (it is not really a secret).

Sincerely yours,

Nikolai V. Ivanov

Timothy Gowers:

ReplyDeleteHere you presented your position as a sort of science-fiction. You say that you "believe that computers...", that you "imagine a brief golden age...".

Of course, there is no need to argue with your imagination. I like novels and movies about super-human and super-intelligent cyborgs or distributed super-intelligent "computers". Not because I find such stories plausible, but because they help to understand humans. One may discuss if your ideas may serve as a good concept for a sci-fi novel or a movie. But I am sure that you are talking about something much more substantial than a concept invented to pitch a project to a studio executive.

You also "believe" that something will happen. It seems to me that your beliefs are not of a religious nature, and hence one can argue about them. I do not share these beliefs. It seems to me that our beliefs are different because we have different ideas both about mathematics and about the humans. In fact, this blog is mainly about these differences till now, with few digressions into the current affairs.

One thing should be pointed out right away: I do not see mathematics as a "kind of career". Its significance is deeper. And for a human mathematics needs to be a calling, not a career choice. As a career, it is not attractive at all. I would advise against it, if it is

. For a short period of time and for very few people it was attractive. This time is gone.a choiceBut the heart of the matter is left out of your comment. You do not just imagine things, or believe in something. You are working toward a realization of your beliefs.

It is kind of paradox, but I consider your projects especially dangerous because they cannot be realized - if the mathematics is understood the way I do understand it. You wrote a lot about the way the mathematician of the "second culture" are doing mathematics. The your "golden age" computers would help such mathematician, I agree. They will not help me. But you do not say "my mathematics", you say simply "mathematics".

Your ideas may prevail only if your kind of mathematics and the "second culture" mathematicians will push away the kind of mathematics I admire most and the mathematicians who work the way I work (there are ones who are infinitely better than me, and I am really concerned about them, not about myself). And this is a very real perspective. The "second culture" mathematicians will simple take all available positions, and the new generation will work in their style.

Mathematical fashions are much stronger than fashions in clothing, and they change much slower. The mathematics of the "second culture" - here I mean more or less a tautological thing, the research for which knowing an obscure lemma in an obscure paper may be crucial - is taking over, it seems.

To be continued.