No, I will not write about the famous book by Lakatos. I will write about proofs, or rather “proofs”, since what we see in math journals are often not really proofs.
This week I read two texts by two different people, which confirm what I’ve been thinking for some time already. I have to say that reading through papers in math journals can be pretty frustrating. And it’s not because I’m stupid and can’t understand the proofs (well, this, too, sometimes), but the main reason is that there are so many published papers with errors. Seemingly some mathematicians just don’t care whether their “results” are true or not; a grant is a grant, a published paper is a published paper, and who cares about correctness, right? (I know that this seems harsh. But I have, ekhm, proofs, like papers with errors, and sometimes quite obvious ones. And it’s not like there’s one paper in a hundred which contains mistakes. I will return to the question of percentage of erroneous articles later in this post.)
One can wonder, what’s the problem – why is that so? In his book on philosophy of mathematics, Professor Batóg wrote (I don’t have the book now, so I’m quoting from memory):
Having the apparatus of formal mathematics, the only reason the mathematicians’ papers can contain errors is laziness.
It turns out that it might be the case that there is another reason (which, by the way, is no excuse): mathematical notation is not as good as many think it is. Here’s what Gerald Sussman (yes, that Gerald Sussman) says about it, from a teacher’s perspective:
Mathematical notation fundamentally sucks. […] Mathematicians have
not been very careful about notation. […] Mathematical notation
is in fact an impressionistic natural language, which is thereby no good
for teaching elementary stuff.
What Sussman proposes instead – and what he actually used in his Structure and Interpretation of Classical Mechanics – is using actual executable code in a programming language (not hard to guess which one, knowing who Sussman is
) instead of the sloppy notation usual in mathematics. I have yet to look at his book, but I find the idea interesting.
And then I learned about an even stronger claim about the way mathematicians do their writing, by Leslie Lamport (yes, that Leslie Lamport):
[…] mathematical notation has changed considerably in the last few centuries. Mathematicians no longer write formulas as prose, but use symbolic notation such as e^{i\pi}+1=0. On the other hand, proofs are still written in prose pretty much the way they were in the 17th century. The proofs in Newton’s Principia seem quite modern. This has two consequences: proofs are unnecessarily hard to understand, and they encourage sloppiness that leads to errors.
However, it is as silly to express logical proof structures in words as it is to express equations in words.
Lamport cites some anecdotal evidence suggesting that about 30% (!) of math papers contain errors. In fact, he also goes further: not only does he notice the problem, but also proposes a solution. One part of the solution is what he calls “structured proofs”. They are still not fully formalized, but are much closer to that ideal, and Lamport claims that they are much better than the usual ones. For instance, rewriting a proof in this way allowed him (more than once!) to find a subtle error.
The latter part of the proposed solution is writing fully-formalized proofs. In fact, his solution more or less coincides with my intuition that the future of mathematics lies in machine-checked proofs. Of course, writing such proofs is somewhat harder than what we are doing now. But consider the man-hours saved when there is no need to talk about a result during a seminar just to double-check the proof, only to discuss what is already checked and known to be true. Imagine that the referee’s work will no longer consist in checking the details of proofs, but discussing the importance of the results of the paper. I would like to live in that future. Is it possible? Lamport goes on to write:
Most mathematicians have no idea how easy it is to formalize mathematics. Their image of formalism is the incomprehensible sequences of symbols found in Principia Mathematica. The appendix contains formal TLA+ definitions of intervals, limits, continuity, and the derivative, assuming only the definitions of the real numbers and of ordinary arithmetic operations. I expect most readers will be surprised to learn that this takes only 19 lines. The appendix also contains a TLA+ proof of Spivak’s corollary that has been checked by the TLAPS proof system.
In fact, he proposes that we should use fully formalized proofs to teach mathematics. I can’t agree more. I spent numerous hours trying to explain to students some “basic” stuff, which – as it turned out again and again – is far from “basic”, “obvious”, “trivial” etc. I also remember my horror when I started studying differential equations, when what I hoped would be a rigorous treatment was full of hand-waving and plain cheating. (If you find this claim too bold, listen to Sussman’s talk, when he quotes Michael Spivak saying more or less the same about the notation in multivariable calculus. I hear that it looks similar in some other areas of mathematics, too.) Here’s one more quotation from Lamport:
Learning to write structured formal proofs that a computer can check will teach students what a proof is. Going from these formal proofs to structured informal proofs would then be a natural step.
Is it crazy to think that students who cannot learn to write proofs in prose can learn to write them in an unfamiliar formal language and get a computer to check them? Anyone who finds it crazy should consider how many students learn to write programs in unfamiliar formal languages and get a computer to execute them, and how few now learn to write proofs.
Definitely, both proposals are something worth trying. At least I’m going to try. I would like to give here more quotes from Lamport’s paper, but this doesn’t make sense: it’s available on the net, so go read that paper. Now. It’s well worth it.