No, the Penrose-Lucas argument does not demonstrate any such thing quite clearly. In fact, the argument was refuted in print before Lucas ever published it, in

No, the Penrose-Lucas argument does not demonstrate any such thing quite clearly. In fact, the argument was refuted in print before Lucas ever published it, in a nice paper called "Minds and machines" by Hilary Putnam. Exactly where it fails depends on exactly how it's stated, but here's a sketch: Goedel proved that a formal system powerful enough to talk about mathematics either is inconsistent or else cannot prove its own consistency. Lucas and his followers claim that human mathematicians have no such limits; presented with such a system they can just see that it's consistent. In Lucas's version we look at some particular candidate system that might implement a human being, and just see it's consistent. In Penrose's version we look at mathematics as a whole and just know it's consistent. But this is all nonsense. Real human mathematicians don't look at the sort of system that might implement a human being (still less, the totality of all mathematicians working together) and "just see" it's consistent. They don't even look at the nice streamlined formal systems they've made specifically for doing formalized mathematics in and "just see" that. Frege's system was inconsistent and he didn't notice after writing two volumes on it. (Russell famously pointed out an inconsistency.) Quine's ML was inconsistent and he didn't notice until Wang pointed it out. For all we know there might be some inconsistency lurking in ZF; it seems like a very good guess that there isn't, but that's all. And, I repeat, those are highly streamlined systems that don't attempt to do anything nearly so complicated as describing the complete behaviour of an actual mathematician's mind. We do sometimes attempt to study computer hardware and software -- systems a bit more like actual human minds, but still orders of magnitude simpler -- using formal methods. Sometimes we try to prove them correct. These proofs are also often wrong, which is why hardware and software have bugs. (In some cases we're pretty confident about relatively large systems; guess what?, the correctness proofs for those are done by computer and there's no "just seeing" about them.) The idea that a human being could look at a formal system representing the entirety of what their brain does and "just know" that it's consistent is not just wrong, it's one of the wrongest things any otherwise intelligent human being has ever suggested. But that is (part of) what it would take to show that the formal system didn't really model them perfectly. This is far from being the only major error in the Lucas-Penrose argument, but it's the worst one.