Thus far, formalized mathematics seems an unpromising idea. Bourbaki may be right that such formalization is simply impractical for people to do. In any case, as [naur-pvf] points out, formalization sometimes leads to more errors, not fewer, as the underlying intuition which provides a check on correctness begins to get lost --- so even one of the claimed merits of formalization is open to question. The problems of formalization have been well put by [constable-programs]:
It is thus possible to translate the proof of any mathematical theorem into a completely formal proof. However, the prospect of actually doing this is quite daunting because an informal proof of modest length will expand to a formal one of prodigious size and will require in its production extreme care and detailed knowledge of the more or less arbitrary conventions of the particular formalism. These tedious details will in sheer number dominate the interesting mathematical ideas which are the raison d'être of the proof.
But like the authors just quoted, we believe that the arrival of the computer changes the situation completely, for several reasons.
It isn't very surprising that the computer should make such a dramatic difference; after all it has revolutionized work in many scientific disciplines. Previously unthinkable ideas like detailed simulations of weather systems have become possible --- formalizing mathematics in a deductive calculus demands fairly modest computer power by comparison.
So thanks to the computer, we may at last be able to do something about the lack of formality in ordinary mathematics. This would be welcome to 'hawkish' logicians18 like [nidditch], who complained that 'in the whole literature of mathematics there is not a single valid proof in the logical sense', but perhaps not to people such as [demillo-social] who regard the conventional 'social mechanisms of the mathematical community' as the only real means of establishing a valid proof. We do not agree with either of these extreme positions. Regarding the latter, we think that social processes may just be a necessary evil resulting from the difficulty (hitherto) of producing formal proofs.19 Compare the enthusiasm among the Greeks for deciding scientific questions by a social process rather than empirically, a tendency that survived until about Descartes.