[FOM] The Role of Formalization

[henriknordmark@mac.com]

Recently, there has been a fair amount of interesting discussions about 
the scope of mathematics and about mathematical rigor. This reminded me 
of an anecdote of a student of axiomatic set theory who insisted in 
writing all of his proofs for homework exercises in a extremely 
rigorous fashion. All of his proofs were symbolic and with the 
appropriate software these proofs could probably have been checked by a 
computer. The grader was a bit confused as to what to do with these 
proofs since they were correct and very rigorous but it was not really 
what was expected from him. After a while, the professor and the grader 
recognized the fact that it was in some sense admirable that he wrote 
his proofs so formally, but requested him to start writing his proofs 
at a higher level of abstraction, which was more appropriate for 
human-readability.

I think this points out the interesting fact that although we strive 
for all of our Mathematics to be formalizable for reasons of rigor, 
most mathematicians are not really that interested in having formal 
symbolic proofs of their theorems.

There is of course some interest in formal symbolic proofs of our 
current mathematical knowledge. The QED project and the Mizar project 
attest to this.
http://www-unix.mcs.anl.gov/qed/


However, this type of work does not seem to interest too many 
mathematicians and perhaps for good reasons.
Is there a need for a repertoire of formal symbolic proofs? Is it in 
some sense mathematically interesting to provide symbolic proofs of our 
current mathematical knowledge? Is it worth investing time and money 
for such an endeavor? Would we be able to gain any new insights by 
doing this? Will future generations in any way profit from having a 
repertoire of symbolic proofs at their disposal?



Henrik Nordmark
Institute for Logic, Language and Computation
Universiteit van Amsterdam
www.homepage.mac.com/henriknordmark