[solomatov]

>Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems.

They don't prove theorems. You do this by writing a program.

[JadeNB]

Sure, but, regardless of agency, human or automated, it is still not possible to prove all true theorems. (The human / automated distinction comes in more sharply in the halting problem, where any potential halting decider will choke on some program that proveably terminates.)