Peter Krautzberger on the web

Formal proofs are our democracy

Reading papers can lead to horrible acts. Today, I felt like mutilating a famous quote.

Sir Winston Churchill
Sir Winston Churchill. Source: Library of Congress, via Wikipedia.

Many forms of communicating mathematics have been tried and will be tried in this world of sin and woe. No one pretends that formal proofs are perfect or all-wise. Indeed, it has been said that formal proofs are the worst form of communicating mathematics except all those other forms that have been tried from time to time.

When I come up with a mathematical result, I have the strong urge to share it, to communicate it. As a trained mathematician, I resort to the established mode of communication, formal proof.

This has two problems.

Formalizing is tricky

On the one hand, I might will make a mistake formalizing my thoughts. Of course, we mathematicians are in the terrible habit of finding that perfectly acceptable (have you noticed that there are no retractions in mathematics because of mistakes?). Almost all the time, even though a formal proof might be wrong or incomplete, it’s considered fixable and the result “essentially” correct (case in point: Perelman). It seems a majority agrees that there’s much more to a mathematician’s result than what might be written on paper.

In the same vein but much worse is the effect of formal proof on mathematical writing. Most papers are badly written and most proofs are written the wrong way around (like \varepsilon - \delta proofs that start with a choice of \delta ) or badly structured in other ways. It seems a lot of people are not aware that a formal proof is a miserable tool for communicating mathematics and has to be used very carefully to facilitate communication. Such care would, of course, clash with the all-encompassing publish-or-perish pressure that has led to the terrible style of “getting the least publishable unit passed a referee with minimal effort”.

All of the above is really just one big problem and luckily it is one that could be fixed by a functioning scientific community (unluckily, it most likely won’t be fixed).

Formalizing is impossible

The second problem however seems intrinsic and unsurmountable.

Moby Dick attacking a skiff
Both Jaws, like enormous shears, bit the craft completely in twain. — Page 510. Source: Wikipedia.

Formal proofs cannot capture what I think when I think mathematics. The problem is that I cannot share my mathematical insights in their entirety since they are a complex combination of rational and emotional thought, intuitions, memory, successful failures and so on.

There might be a way to overcome this problem. Then again, there might be a better form of government than democracy.