The Penrose–Lucas argument 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?
 A: Shapiro (in Philosophia Mathematica (III) 14 (2006), 262–264) published a review of Torkel's book, here referred to by Gerry Myerson:

Of course, some alleged applications and consequences of
  incompleteness cannot be dismissed as easily as this. The
  Lucas-Penrose thesis (or theses) do not seem to turn on such
  elementary misunderstandings of what the incompleteness theorems say.
  Lucas and Penrose themselves certainly understand the mathematics. The author’s treatment of the issue provides a nice introduction to
  the underlying issues, but the book does not contain many references
  to the extensive literature on this topic.
I suspect that most readers of this journal do not need this book.
  Those who engage in contemporary debates concerning the philosophy of
  mathematics knowfull well what the incompleteness theorems say and
  what they do not say." (bold letters are mine)

That the book of Torkel falls short in addresing this issue, is quite clear. Now, to say that the problem concerns exclusively to math, confines math to a kind of closed crystal box because there are major issues in cog-sciences regarding math and logical knowledge to be explained. It might be due to phenomena such as this one here raised by Penrose and others, that social sciences in general seem so chaotic and underdeveloped in comparison to math, physics, chemistry and other comparable fields of research.
The last point I wish to bring to your attention here is the one that Clinton himself acknowledges: 

(1) Humans are proving incompleteness not using the system itself, but using some greater system. 

If this is true, then how exactly functions our mind or brain to be able to prove such a thing ever from a greater system?
A: There is big confusion in the formulation here. It does not take a human mathematician to prove the incompleteness theorem, because it is a theorem of arithmetic, which a proof ckeching software might check. What this theorem says, is that if a theory T defined in some way is consistent, then its Gödel sentence is unprovable in T but actually a true sentence because it turns out to be logically equivalent to the claim of consistency of the theory defined in the same way. So we find G to be true when T is consistent, just because it is an equivalent expression of the premise of this implication ! 
"If there is a proof of incompleteness that was found in the system by a human" you mean a proof of G, that is a proof of consistency of T ??? but the incompleteness theorem shows that if the claim G of consistency of T was provable from T, then T would actually be inconsistent !!!
Now for the Penrose-Lucas argument itself, it does not work but I found another anti-mechanist argument related with the incompleteness theorem, which I consider much more solid.
A: In (belated) response to your two points more specifically:
1) I suppose the point is that humans are somehow able to identify their own formalisation, F, which they are then able to form a Godel sentence G(F) from. They can't use a greater (or lesser) system than the one they are using.
2) The incompleteness theorems don't provide a formal proof of incompleteness, per se. If they did then your argument would follow. They provide an argument of incompleteness that sits 'outside' the formalism under inspection. The Godel sentence G(F) is constructed to be true but not provable by F. It's true that this doesn't mean that another formal system, H, couldn't prove the statement G(F). But we're concerned in particular with the system F and whether it really captures our conscious reasoning.
You can read more on the IEP:
http://www.iep.utm.edu/lp-argue/#H3
A: I recommend Torkel Franzen's book, Godel's Theorem, for pretty much anything concerning popular misconceptions, but in particular there is a discussion of Penrose, pages 119 to 124. 
