Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand

In one of Krylov’s fables, a small dog Moska barks at the elephant who pays no attention whatsoever to Moska. This image comes to my mind when I think of constructive mathematics versus “classical” (that is mainstream) mathematics. In this article, we put a few words into the elephant’s mouth. The idea to write such an article came to me in the summer of 1995 when I came across a fascinating 1917 bet between the constructivist Hermann Weyl and George Polya, a classical mathematician. An English translation of the bet (from German) is found in the article.

Our main objection to the historical constructivism is that it has not been sufficiently constructive. The constructivists have been obsessed with computability and have not paid sufficient attention to the feasibility of algorithms. However, the constructivists’ criticism of classical mathematics has a point. Instead of dismissing constructivism offhand, it makes sense to come up with a positive alternative, an antithesis to historical constructivism. We believe that we have found such an alternative. In fact, it is well known and very popular in computer science: the principle of separating concerns.

[Added in July 2006] The additional part on computer proofs vs. proofs by hand was a result of frustration that many computer scientists would not trust informal mathematical proofs, while many mathematicians would not trust computer proofs. I seemed obvious to me that, on large scale, proving is not only hard but also is imperfect and has engineering character. We need informal proofs and computer proofs and more, e.g. stratification, experimentation.