ABSTRACT
There are several aspects of the thesis that mathematical reasoning is mechanical. It means more than the thesis that mathematical arguments can be formalized; it requires mechanization of methods of proof and not merely formalization of given informal proofs into a mechanically checkable form. An ambiguity in this thesis is the difference between the possibility of somehow doing mathematics mechanically and the stronger requirement of mechanizing the actual process of doing mathematics. For example, according to the second interpretation, the thesis would have us mechanize the processes of how individual mathematicians find proofs, how mathe matics is taught, how the mathematical community reaches a consensus about accepting certain results (as true). If the interest is to determine whether the thesis can conceivably be true, there are advantages in taking the thesis in the second sense. If one wishes to do as much mathematics as possible with computers, then it is reasonable not to worry over being faithful to how people do mathematics. Here we have a special case of the contrast between artificial intelligence and simulation.
