Written: July 15, 2014
One of today's greatest philosophers of mathematics (and science), Ian Hacking has recently published a wonderful book entitled "Why Is There Philosophy of Mathematics At All?".
It is full of wonderful insights, and unlike most philosophers, who are oblivious to the attitudes of current, living, mathematicians, he actually takes them seriously, in spite of their philosophical naïveté [Would you ask a frog about the meaning of being a frog?].
One quote that I particularly liked was (Ch. 7, section 7, p. 232)
``The world has moved on. You cannot have the same attitude to the Folies Bergère (or to dancing girls) that contemporaries of Manet had when he painted the woman behind the bar in 1882; you cannot have the same attitudes to mathematics that philosophically minded German mathematicians had in the same decade.''
And indeed, the world has moved on, but the subworld of mathematics much slower than its complement. Both Alain Connes and Tim Gowers, with their opposing mathematical `philosophies' and attitudes (platonism vs. anti-platonism), and even forward-looking Vladimir Voevodsky, a champion of automated theorem proving, are still in the dark ages of proof-centered dogmatism. Wake up! There are so many interesting mathematical discoveries out there, and only a tiny fraction of them could be ever proved completely, even with the help of machinekind, so the time is ripe to stop wasting our (and our computers'!) time in trying to find `formal proof'. From now on, let's make rigorous proofs optional, and be content with mathematical knowledge that is true with probability 1-10-100.
I am sure that this would be the attitude in one hundred years, so why wait? Let's start to adopt it right away!