“One thing that we conclude from all this is that the 'learning robot' procedure for doing mathematics is not the procedure that actually underlies human understanding of mathematics. In any case, such bottom-up-dominated procedure would appear to be hopelessly bad for any practical proposal for the construction of a mathematics-performing robot, even one having no pretensions whatever for simulating the actual understandings possessed by a human mathematician. As stated earlier, bottom-up learning procedures by themselves are not effective for the unassailable establishing of mathematical truths. If one is to envisage some computational system for producing unassailable mathematical results, it would be far more efficient to have the system constructed according to top-down principles (at least as regards the 'unassailable' aspects of its assertions; for exploratory purposes, bottom-up procedures might well be appropriate). The soundness and effectiveness of these top-down procedures would have to be part of the initial human input, where human understanding an insight provide the necesssary additional ingredients that pure computation is unable to achieve.

In fact, computers are not infrequently employed in mathematical arguments, nowadays, in this kind of way. The most famous example was the computer-assisted proof, by Kenneth Appel and Wolfgang Haken, of the four-colour theorem, as referred to above. The role of the computer, in this case, was to carry out a clearly specified computation that ran through a very large but finite number of alternative possibilities, the elimination of which had been shown (by the human mathematicians) to lead to a general proof of the needed result. There are other examples of such computer-assisted proofs and nowadays complicated algebra, in addition to numerical computation, is frequently carried out by computer. Again it is human understanding that has supplied the rules and it is a strictly top-down action that governs the computer's activity.”