In the twenty three centuries since Euclid mathematical proofs have gradually become more formalised. The ultimate step in formalisation is proofs which can be, and indeed are, checked entirely mechanically.
There are a few advantages to such proofs. Informal proofs rely on intuition. Intuition is often wrong. More subtly, it is often correct, but only on a particular interpretation. But theories, if formulated sufficiently generally, may admit multiple interpretations. This can be quite useful. For example, much of elementary algebra works equally well regardless of whether the numbers in question are rational, real or complex. Mechanically checked formal proofs can ensure that conclusions of theorems follow from their hypotheses under any interpretation which is consistent with the axioms and rules of inference, not just a particular interpretation. They will continue then to hold under interpretations which would never have been considered by the original writer and readers of a proof. Projective geometry, for example, was originally developed for perspective drawing, but is now principally used in settings like error-correcting codes with “lines” and a “plane” with only finitely many points. This is possible because the theory was formulated in a way which didn’t exclude this unanticipated interpretation, and proofs were given for the major theorems which did not rely on any intuition that lines or planes must be infinite.
There are, however, three disadvantages to completely formalised mathematics.
The first disadvantage is that such arguments are hard for humans to read. There is simply too much detail. The language required to remove all ambiguities is too unfamiliar. It is too difficult to identify the important steps. Here, for example, is a formal proof that two times two equals four, in a formal system we will encounter later. \[ \begin{array}{l@{\hspace{2mm}}l@{\quad}l@{\hspace{2mm}}l} 1. & \{ ∀ x . [ ( x · 0 ) = 0 ] \} & 17. & \{ [ ( 0 '' · 0 ) + 0 ' ] = 0 ' \} \\ 2. & [ ( 0 '' · 0 ) = 0 ] & 18. & \{ [ ( 0 '' · 0 ) + 0 ' ] ' = 0 '' \} \\ 3. & [ ( 0 '' · 0 ) ' = 0 ' ] & 19. & \{ [ ( 0 '' · 0 ) + 0 '' ] = 0 '' \} \\ 4. & [ ( 0 '' · 0 ) '' = 0 '' ] & 20. & [ ( 0 '' · 0 ' ) = 0 '' ] \\ 5. & [ ∀ x . ( ∀ y . \{ ( x · y ' ) = [ ( x · y ) + x ] \} ) ] & 21. & \{ ( 0 '' · 0 '' ) = [ ( 0 '' · 0 ' ) + 0 '' ] \} \\ 6. & ( ∀ y . \{ ( 0 '' · y ' ) = [ ( 0 '' · y ) + 0 '' ] \} ) & 22. & ( ∀ y . \{ [ ( 0 '' · 0 ' ) + y ' ] = [ ( 0 '' · 0 ' ) + y ] ' \} ) \\ 7. & \{ ( 0 '' · 0 ' ) = [ ( 0 '' · 0 ) + 0 '' ] \} & 23. & \{ [ ( 0 '' · 0 ' ) + 0 '' ] = [ ( 0 '' · 0 ' ) + 0 ' ] ' \} \\ 8. & ( ∀ x . \{ ∀ y . [ ( x + y ' ) = ( x + y ) ' ] \} ) & 24. & \{ ( 0 '' · 0 '' ) = [ ( 0 '' · 0 ' ) + 0 ' ] ' \} \\ 9. & ( ∀ y . \{ [ ( 0 '' · 0 ) + y ' ] = [ ( 0 '' · 0 ) + y ] ' \} ) & 25. & \{ [ ( 0 '' · 0 ' ) + 0 ' ] = [ ( 0 '' · 0 ' ) + 0 ] ' \} ) \\ 10. & \{ [ ( 0 '' · 0 ) + 0 '' ] = [ ( 0 '' · 0 ) + 0 ' ] ' \} ) & 26. & \{ [ ( 0 '' · 0 ' ) + 0 ] = ( 0 '' · 0 ' ) \} \\ 11. & \{ ( 0 '' · 0 ' ) = [ ( 0 '' · 0 ) + 0 ' ] ' \} & 27. & \{ [ ( 0 '' · 0 ' ) + 0 ] = 0 '' \} \\ 12. & \{ [ ( 0 '' · 0 ) + 0 ' ] = [ ( 0 '' · 0 ) + 0 ] ' \} & 28. & \{ [ ( 0 '' · 0 ' ) + 0 ] ' = 0 ''' \} \\ 13. & ( ∀ x . \{ [ x + 0 ] = x \} ) & 29. & \{ [ ( 0 '' · 0 ' ) + 0 ' ] = 0 ''' \} \\ 14. & \{ [ ( 0 '' · 0 ) + 0 ] = ( 0 '' · 0 ) \} & 30. & \{ [ ( 0 '' · 0 ' ) + 0 ' ] ' = 0 '''' \} \\ 15. & \{ [ ( 0 '' · 0 ) + 0 ] = 0 \} & 31. & [ ( 0 '' · 0 '' ) = 0 '''' ] \\ 16. & \{ [ ( 0 '' · 0 ) + 0 ] ' = 0 ' \} \end{array} \]
The second difficulty with formal proofs is that we need to know that the formal system in which we are working, and the proof checker we use to verify the proofs, are correctly designed. In order to have any confidence in the results, this needs to be proved, but how? We can give an informal proof, or we can give a formal proof, but this would have to be done in another formal system, and checked by a different proof checker, since the correctness of this one has yet to be established. So eventually even the most formal of proofs has to be based on an informal foundation. The gain from using formal systems is therefore not in getting rid of all appeals to human intuition, but rather in reducing those to a tightly defined core. There is also the matter of checking that the formal statements being proved have the desired meaning under the interpretation we’ve adopted for statements in the system, which is in fact a frequent source of error.
The third difficulty with formal proofs is that they can’t accomplish the purpose for which they were originally intended. It was originally hoped that one could find a formal system in which it would be possible to formulate and prove all true statements in mathematics, and of course only true statements, since a system which proves false statements is not of much use. It’s now known that this can’t be accomplished even for arithmetic. Any system which is consistent, in the sense that it cannot be used to prove contradictions, will be incomplete, in the sense that not all true statements will be provable.
This doesn’t mean that formal proofs are useless. The exercise of giving a formal proof that a piece of code works for all allowed inputs, for example, will almost always reveal that it doesn’t. A large scale project was conducted in 2009 to show that the L4 microkernel was free of bugs, in the sense that it was proven to implement its design specification. The exercise uncovered a large number of previously unsuspected bugs, which were then fixed. Some of these were bugs in the implementation, but others were bugs in the specification itself, where assumptions which should have been explicit had been left unstated.