hese. This would probably t ake t he form of pro gr amming the machi ne to do ever y kind of job t hat could be don e, as a mat t er of principle, whether it wer e economica l to do it by machine or not. Bit by bit one would be a ble t o allow t he machine t o make more and more 'choices' or 'decis ions'. On e would event ually find it possible to pro gram it so as to make its behavior be the logical result of a comparat ively small numb er of gene ral principles. When t hese became sufficiently

y important st rand of work in the subject since the sixties has b een devoted t o various attempts to prevent running out of time or memory. These attempts will be discussed in the sect ion "Searching for proofs" below. 21 Kinds of M athematical R easoning 8 In this section we abandon the historical approach to the subject . Instead , we examine the mechanization of mathematics by t aking inventory of the mathemat ics to be mechanized . Let us make a rough taxonomy of mathematics. Of course

_ x 29 + x 3 I _ x 32 + X 34 _ x 36 + x 38 _ x 39 + x 4 I _ x 43 + X 45 _x 46 + X 48 _ x 50 + X 5 I _ X 53 + X 55 _ X 57 + x 58 _ x 60 + x 62 _ X 64 + x 65 _ x 67 + x 68 _ x 71 + x 72 _ X 74 + x 75 _ x 78 + x 79 _ X 8 I + X 82 _ x 88 + x 89 _ x 95 + x 96 ) T his was not done by t r ial and error. It uses algor it hms for polynomial fact orlzat ion" t hat first fact or t he polynomi al mod p for various small primes p, a nd t hen put t he result s together cleverly, using a 19 t h -century t

well known is Myhill's 1970 work [49], in wh ich he demonstrates a recursi ve funct ion, f (t) , whose continuous der ivati ve, df / dt , is non-recursive. Myhill 's fun ction is not hyp ercomput ational in it self, but can be used to produce a hypercomputational system . We imagine two compon ents connected in series. The first is a Turing machine programmed t o generate Myhill's function, while t he second is an analo g comp one nt t hat differentiates its input. Such a combined syst em seems

exec uted in finit e time goes back at least as far as Zeno , an d in t he context of hyper computational syst ems it has been introduced several t imes indep endently (Gold [17] ; Putnam [60] ; Boolo s and J effrey [2] ; Stewart [83,84]). An ATM , or A ccelerating Turing Machine [4,5] , is one in which each instruction is performed in progressively less tim e than its predecessor, so that an infinite computation can run to completion in finite time. Formally, if we suppose that t he n 'th