Gödel’s theorem is a red herring
No matter what game we take Lucas to be playing, Gödel’s theorem is not the real issue. In fact, Gödel’s theorem is a red herring that distracts us from the real issue of transfinite counting (see detailed text).
We can't actually know the truth of the Gödel formula, we can only believe it is based on our belief that the formal system is consistent—a fact that itself can't be proved without contradicting Gödel's second theorem.
Recognising the first point, we can see that it was not the Gödel formula that was the core of Lucas's argument; the real issue was transfinite counting. But Lucas can't prove that he is better at transfinite counting a machine is.
Irving J. Good (1967).
Red herring: An argument that distracts attention from the issue in question. Derives from the use of red herrings—a kind of smoked fish—to distract tracking dogs from the trails of escaped prisoners.