For most of this century it has been known how complete rigour could be achieved in mathematics using formal proof in first order set theory. Because of the complexity of fully formal proofs this has scarcely ever been done, but the standard of proof has been influenced by well developed intuitions about what could be formalised in this way (see for example: The Bourbaki View). | Since the invention of the digital computer the possibility has arisen that with the aid of computers formalisability in principle could be replaced by formalisation in fact (see John Harrison: Enter the Computer). Computers have been used in limited ways for finding and/or checking detailed formal proofs since the 1950's and work continues on the software technologies necessary to support formalised mathematics. |
At the conclusion of the rigourisation of analysis and the formalisation of mathematics two unprecedented problems were outstanding which still remain with us. Both reflected the unmanageable complexity of doing mathematics in practice to the best known standards of formal rigour. |
The rigourisation of analysis concluded with the establishment of the real number system on a sound theoretical basis. Possibly the reason why it took 2000 years to do this may have something to do with the fact that this was the first number system which had no canonical notation for numbers, and hence no way of exploiting the theory in computations. What happens in practice is a kind of fudge. Computations are undertaken using rational approximations to real numbers. Notations for real numbers can be devised which are faithful to the theory without any fudge. They are complex enough that it is doubtful that any human being will ever make much use of them. Computers on the other hand, could cope nicely, if only someone would develop the software to do the job (see: computing with reals). |
The other "problem" was that a standard of rigour was known to be possible that even the most pedantic mathematicians were unwilling to embrace. Russell and Whitehead demonstrated in Principia Mathematica that mathematics could be developed formally, but they also demonstrated that the complexity of formal derivations is prohibitive. Even now, with the aid of powerful computers, formal demonstrations are thought to cost typically ten times the human effort required to prepare journal standard mathematical proofs. Ultimately cheap processing power and ingenious software may enable computers to produce formal proofs, and this is the dream of present day protagonists of formalised mathematics. Meanwhile we see that in two important respects mathematics has outgrown mere human beings and awaits the mathematical maturity of computing machinery. |