I was looking at the Penrose–Lucas argument as discussed on Wikipedia. It states:
In 1931, the mathematician and logician Kurt Gödel proved that any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. Further to that, for any consistent formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory.
In his first book on consciousness, The Emperor's New Mind (1989), Penrose made Gödel's theorem the basis of what quickly became an intensely controversial claim. He argued that while a formal proof system cannot, because of the theorem, prove its own incompleteness, Gödel-type results are provable by human mathematicians. He takes this disparity to mean that human mathematicians are not describable as formal proof systems, and are not therefore running an algorithm.
If find this hard to believe, because I can't see why either one of the following is true:
(1) Humans are proving incompleteness not using the system itself, but using some greater system
OR
(2) If there is a proof of incompleteness that was found in the system by a human, then as long as that proof is of finite length, it could be found algorithmically simply by trying and checking every proof until one finds one which is correct.
I looked at the criticisms on the Wikipedia page, and they only criticised the science of quantum effects in the brain, not the mathematics of the original assertion.
I'm sure I'm missing something, but is his original assertion correct? And if so, could you explain why?