How does Lucas's argument work?
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&ouml;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.