How does Lucas's argument work?

Question

In Minds, Machines and Gödel (1959), J. R. Lucas shows that any human mathematician can not be represented by an algorithmic automaton (a Turing Machine, but any computer is equivalent to it by the Church-Turing thesis), using Gödel's incompleteness theorem.

As I understand it, he states that since the computer is an algorithm and hence a formal system, Gödel's incompleteness theorem applies. But a human mathematician also has to work in a formal axiom system to prove a theorem, so wouldn't it apply there as well?

Answer 1

Yes, it applies. If a statement cannot be derived in a finite number of steps, then it doesn't matter if the person trying to prove it is a human or a computer.

The mathematician has one advantage over a standard theorem proving algorithm: the mathematician can "step out of the system" (as Douglas Hofstadter called in Gödel, Escher, Bach), and start thinking about the system. From this point of view, the mathematician may find that the derivation is impossible.

However, an AI for proving theorems could be programmed to recognize patterns in the derivation, just like our hypothetical mathematician, and start reasoning about the formal system to derive properties of the formal system itself. Both the AI and the mathematician would still be bound by the laws of mathematics, and not be able to prove a theorem if it was mathematically improvable.

Answer 2

After he lays out his argument, he deals with some counterarguments. The following looks like the weakest one to me:

We can use the same analogy also against those who, finding a formula their first machine cannot produce as being true, concede that that machine is indeed inadequate, but thereupon seek to construct a second, more adequate, machine, in which the formula can be produced as being true. This they can indeed do: but then the second machine will have a Gödelian formula all of its own, constructed by applying Gödel's procedure to the formal system which represents its (the second machine's) own, enlarged, scheme of operations. And this formula the second machine will not be able to produce as being true, while a mind will be able to see that it is true. And if now a third machine is constructed, able to do what the second machine was unable to do, exactly the same will happen: there will be yet a third formula, the Gödelian formula for the formal system corresponding to the third machine's scheme of operations, which the third machine is unable to produce as being true, while a mind will still be able to see that it is true. And so it will go on.

In short, by making the system more complex, it can see the inadequacy of a less complex system, but a yet more complex system can see its inadequacy. But from whence comes the claim that a mind could see the inadequacy in the nth machine? If, say, the Gödelian formula had as many components to it as a human brain had neurons, it seems suspect to claim that the human could evaluate that formula and identify that it is in fact a Gödelian formula, rather than a similar but not quite identical sentence.