Informal rigor and mathematical understanding (Q4364503)

This paper maintains that there are rigorous, non-formal mathematical proofs. Moreover, to say that they are rigorous is not merely to say that in principle they could be fully formalized; indeed, such a formalization would, in all likelihood, loose something that is essential to much mathematical demonstration, most especially a quality of obviousness. Mathematical proofs are supposed to serve two ends, guarantee of truth and explanation. It is the latter aspect that is poorly served by formalization. The argument here is by example. Two `experiments' are presented in which one can see how a result is achieved informally, assisted by diagrams, and why it works as it does, but which would resist formalization. This is essentially an exercise in the phenomenology of mathematics. How effective it is may depend on the strength of one's intuitions and imagination. While it may be that the informal argument accomplishes the explanation sought, it is not discussed how the other aspect of guarantee is achieved. Similar procedures applied to other problems are notoriously fallible. For the entire collection see [Zbl 0870.00023].