“There is one are of work that should be mentioned here, referred to as 'automatic theorem proving'. One set of procedures that would come under this heading consists of fixing some formal system H, and trying to derive theorems within this system. We recall, from 2.9, that it would be an entirely computational matter to provide proofs of all the theorems of H one after the other. This kind of thing can be automated, but if done without further thought or insight, such an operation would be likely to be immensely inefficient. However, with the employment of such insight in the setting up of the computational procedures, some quite impressive results have been obtained. In one of these schemes (Chou 1988), the rules of Euclidean geometry have been translated into a very effective system for proving (and sometimes discovering) geometrical theorems. As an example of one of these, a geometrical proposition known as V. Thebault's conjecture, which had been proposed in 1938 (and only rather recently proved, by K.B. Taylor in 1983), was presented to the system and solved in 44 hours' computing time.

More closely analogous to the procedures discussed in the previous sections are attempts by various people over the past 10 years or so to provide 'artificial intelligence' procedures for mathematical 'understanding'. I hope it is clear from the arguments that I have given, that whatever these systems do achieve, what they do not do is obtain any actual mathematical understanding! Somewhat related to this are attempts to find automatic theorem-generating systems, where the system is set up to find theorems that are regarded as 'interesting'-according to certain criteria that the computational system is provided with. I do think that it would be generally accepted that nothing of very great actual mathematical interest has yet come out of these attempts. Of course, it would be argued that these are early days yet, and perhaps one may expect something much more exciting to come out of them in the future. However, it should be clear to anyone who has read this far, that I myself regard the entire enterprise as unlikely to lead to much that is genuinely positive, except to emphasize what such systems do not achieve.”