Penrose's argument does not require humans to prove every true statement. It is of the form - "Take a program P which can do whatever humans do and lets a gener

Penrose's argument does not require humans to prove every true statement. It is of the form - "Take a program P which can do whatever humans do and lets a generate a single statement which P cannot do, but humans can." The core issue is that P has to seen to be correct. So, the unassailable part of the conclusion is that knowably correct programs can't simulate humans.