In his paper, "Minds, Machines and Gödel", J.R. Lucas writes the following:
Gödel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.
Contrariwise, the following papers,
Wilfrid Sieg and Clinton Field, "Automated search for Gödel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)
Lawrence C. Paulson, "A Mechanized Proof of Gödel's Incompleteness Theorems using Nominal Isabelle" (published
suggest that computers can not only show that the Gödel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.
Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Gödel sentence is true. In point of fact, we actually infer the truth of the Gödel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover (via its respective metatheory) can infer the truth of the Gödel sentence, assuming ZF − Infinity is consistent).
So that is the question before us: Can computers that run theorem-proving software infer that that the Gödel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA as the object-theory for their theorem-proving software).
Best Answer
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
[This paragraphs has been made obsolete as the question was edited to address the issue.] Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.