# How does Lucas's argument work?

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?