Written: Feb. 18, 2015
In a beautiful recent masterpiece, discussed in my previous opinion 140, Zvi Artstein claims, very convincingly, that the reason most people (in fact, all of them, including us, professional mathematicians!) find math so hard, is that biological evolution did not prepare us to the rigid discipline of formal mathematical and logical reasoning. In order to survive in the jungle, we had to use informal, intuitive, `Bayesian' `logic', if you would call it logic at all.
But in spite of that, Mathematics blossomed, and has come a long way, both as queen and servant of the physical sciences. For more than two millenia, the cultural evolution of mathematics, and the notions of axiomatic method and rigorous proof ruled. But neither Euclid, nor Gauss, not even Ramanujan, knew about the new messiah, the powerful electronic computer, that would revolutionize both the discovery and the justification of mathematical knowledge, and would (soon!) turn mathematics into an empirical science, just like physics, chemistry, and biology, but dealing with mathematical entities (like numbers, equations, groups etc.) rather than with electrons and stars, (or acids and bases, or cells and genes etc.), and we would soon abandon our fanatical insistence on rigorous proof, and very soon semi-rigorous proofs (see my manifesto) would be fully acceptable, and soon after, completely non-rigorous proofs!
In a recent article, Shalosh B. Ekhad and I present, as case studies, a class of problems where fully rigorous proofs can be safely abandoned. I believe that this would be the case, in at most fifty years, for the rest of mathematics. We will come to realize that fully rigorous proofs are only possible for relatively trivial statements, for example Fermat's Last Theorem, the Poincaré conjecture, and the Four Color Theorem. But for really deep (and interesting!) mathematical knowledge, we would have to be content, if lucky, with semi-rigorous proofs, where we know that a proof exists, but it is too complicated for us, and even for our computers, to find, and more often with fully non-rigorous (heuristic and empirical) proofs.