I postulated that "given the output of program P, you can easily find in it the list of theorems found so far" -- by which I meant that it's easy to write a program that takes the output of P until step t, and returns everything written on the list up to time t (was the confusion that it wasn't clear that this was what I meant?). If you also know the source of P, you have a program that for every t returns the list up to time t, so it's easy to write down the predicate L(n) of PA that says "there is some time t such that the proposition with Gödel number n appears on the list at time t." By the diagonal lemma, there is a sentence G such that

PA |- G <-> not L(the Gödel number of G).

G is humanity's Gödel sentence, and there is no trouble in writing it down inside the simulation, if you know the source of P and the source of the program that reads the list from P's output.

(Well, technically, G is one Gödel sentence, and there could be other ways to write it that are harder to recognize, but one recognizable Gödel sentence should be enough for the "no AI" proof to go through if it were a well-formed argument at all, and I don't think Stuart's claim is just that there are some obfuscated ways to write a Gödel sentence that are unrecognizable.)