On proofs and more

This is a transcript of an exchange on Twitter on what mathematicians and others expect from proofs. (A previous exchange on a different topic is here. Twitter produces surprisingly nice results sometimes. What follows is a bit meandering, but interesting points are made.)

It began at 7:56 am – 27 Jun 13, with the twitter account of Republic of Mathematics (a website started by Gary Davis) quoting from Bill Thurston‘s great essay On proof and progress in mathematics. The quoted sentence was a short excerpt from the following:

The question is not even “How do mathematicians make progress in mathematics?”
Rather, as a more explicit (and leading) form of the question, I prefer “How do mathematicians advance human understanding of mathematics?”
This question brings to the fore something that is fundamental and pervasive: that what we are doing is finding ways for people to understand and think about mathematics.

To this, the account of The True Beauty of Math replied with “[Which is] why computer proofs [are of] little use.” Republic of Mathematics objected to this position, and quoted from an article by Sara Billey titled Computer Proofs. What is the value of computer assisted proofs?. The quoted sentence is an excerpt from:

Some mathematicians have tried to protect their egos by proposing that human proofs are superior to computer assisted proofs. They claim that we don’t learn as much from computer assisted proofs as we do from a human proof. They claim computer proofs can be difficult to verify. They claim computer proofs are less elegant. I find these complaints to be naive.

This was retweeted by Guy Longsworth, which is how I saw it.

I commented:

The point of a proof is really to produce understanding. “Elegance” is one of the ways we describe this.

Guy Longsworth:

That strikes me as very plausible. Thanks! 🙂

Santiago Ortiz added to this:

A proof completed with the use of computers would continue being elegant if the code is elegant.

One can easily see that Santiago is not alone in this view. I highly recommend reading Donald Knuth‘s Computer programming as an art. Nevertheless, this was objected by Morosoph:

Well, the meta-proof would be elegant, but the proof itself would not be, surely?

Me:

It depends, really. Again, at least for me the point is to gain insight.

Morosoph:

So, elegantly coded computer proofs that generate inelegant proofs generate insight, but perhaps less than a direct proof would have done?

Guy Longsworth:

Seems that that could be a feature of a subject matter: being less amenable to insight.

Morosoph:

Perhaps mathematics is the process of extracting insight from logical relations? Then computer proofs would be mathematics of a lower grade, so to speak.

Me:

I don’t agree. Computers are a new tool, we are just getting used to them. No gradations.

I then suggested an example where I feel we use computers fairly routinely, and in my opinion we do not quite yet understand as much as it would be desirable:

1. In number theory, it is common: First, we observe a pattern looking at small numbers.
2. We conjecture that the pattern holds, based on our short list.
3. We work hard, and find a proof, that only applies to significantly large numbers.
4. We then extend our list of small numbers, through extensive computations.
5. This seems to me a proof where the initial pattern was never explained.

(There are many examples of this kind. Since some misunderstanding may occur, of course I am not claiming this is how research occurs in all of number theory, all the time, or even in analytic number theory.)

Meanwhile, Richard Percival replied, somewhat jokingly, to my comment on elegance:

Blimey. I thought elegance was a mere side-issue aesthetic characterisation of something more important.  Now you’re all artists, really. Working with jolly difficult materials.

Me:

One quickly gets in controversial territory.

One of my former advisors scorns the idea of the importance of aesthetic considerations in proofs, as well as the idea of there being a social component to truth in mathematics.

(This is one of those instances where something more detailed would have been ideal. Or, as I commented, “A 140 characters limit has the obvious drawback that muances get shortchanged.” John Steel‘s position is obviously more elaborate. But he definitely feels strongly that talk of art and beauty when discussing mathematics is misguided (Knuth’s article notwithstanding). On the topic of truth in mathematics having a social element, the best reference is What is mathematics, really?, by Reuben Hersch. John, easily the most vocal modern platonist in current set theory, opposes this view strongly.)

Guy Longworth:

I’m inclined to scorn social conceptions of truth. But surely a social element in understanding and insight. 🙂

Richard Percival:

Is it about “understanding” as an end – is that what you seek? “Understanding” vs “discovery”. If understanding, then the mind that understands is central, which gets to social pretty quick.

Me:

 Tricky to say. J. von Neumann: “Young man, in mathematics you don’t understand things. You just get used to them.” But I disagree with him in this regard. On the other hand, there are people like Ramanujan.

As a coda, continuing one of the threads above, Santiago Ortiz asked:

Didn’t Turing and Gödel dissolve the differences between program and proof?

To which Javier Moreno replied:

Only at a highly formal level.

Scott Murray:

Writing code is not so different from writing natural language. Both involve terms and symbols dancing toward order.

If you code, you are a writer.

To which Santiago replied:

Discussing with guys saying that math proofs with programming are not very elegant; disagree! depends if code used is elegant.

Scott Murray:

Absolutely. I doubt they can prove that, in any case. 🙂

Santiago Ortiz:

Elegance can’t be proved and none cares, as @andrescaicedo pointed an elegant proof is insightful, and code can add insight.

Ekene Ijeoma:

Elegant or not, code is a language…

Santiago mentioned a quote from Think Bayes. Bayesian Statistics Made Simple, by Allen B. Downey. The preface opens with:

The premise of this book, and the other books in the Think X series, is that if you know how to program, you can use that skill to learn other topics.

Santiago Ortiz:

Prev. quote is just another good argument that coding is writing, in response to previous discussions in which some claimed that the use of programing removed elegance to math proofs.

Javier Moreno:

Yo no creo que le quiten elegancia pero sí dificultan entender la naturaleza de los fenómenos que demuestran. Son “oscuras”. U “opacas”.

[I do not think that it subtracts elegance, but it difficults understanding the nature of the phenomena it demonstrates. Through a glass, darkly.]

Santiago Ortiz:

Son oscuras si el código es oscuro, son claras si el código es claro.

[Obscure only if the code is obscure. Clear otherwise.]

Javier Moreno:

No, va más allá de la claridad del código. El código puede ser claro, pero el fenómeno subyacente de todas formas opaco.

[No, it goes beyond the clarity of the code. It may be clear, and yet the underlying phenomenon remains opaque.]

Santiago Ortiz:

Eso es como decir que un texto es claro pero lo que cuenta no es claro / código claro implica proceso y resultados claros.

[That’s like arguing that a text is clear but what it tells is no. Clear code implies clear process and results.]

Javier Moreno:

No, Tiene que ver con algo así como la diferencia entre P y NP: posibilidad de verificación de una solución no ofrece “soluciones”. Sin duda alguna son demostraciones formalmente correctas pero son, para las personas que estudian esos problemas, insatisfactorias.

[No; it is akin to the difference between P and NP: The possibility of verifying a solution does not give us in itself a solution. Undoubtedly, the proofs so obtained are formally correct, but the people studying the problems find them unsatisfactory.]

Santiago Ortiz:

Creería que con el tiempo el código se asimilará culturalmente como un lenguaje formal +, y no se percibirá como insatisfactorio.

[I think that eventually code will be accepted culturally as yet another formal language, and this dissatisfaction will pass.]

Javier Moreno:

Fíjese que aunque las lógicas formales andan por ahí hace años y hay teoremas de completez, nadie demuestra nada usando derivaciones lógicas estrictamente formales casi nunca.

[Note that even though we have had formal languages for many years, and there are completeness theorems, almost never something is proved using only formal logical derivations.]

This seems to have been the end of this thread, at 9:26 am – 29 Jun 13.

Advertisement