I came here to say the same thing. I was really interested in Gödel's Incompleteness Theorem in college, and around 22 I had the same idea as Penrose: that if the mind could be simulated on a computer, it would be a formal system in Gödel's terminology, yet the mystery of the Incompleteness Theorem is that we can work out when things are true or false despite limitations of formal systems. Penrose takes that nugget and tries to develop a rigorous argument against general AI or a mind that is explainable by purely Newtonian mechanics. At least that's my understanding. I only made it about half way through the book, because it is not really aimed at a general reader. Agree or not, it's a pretty fascinating argument, one which makes my head spin.
Some other nice resources on Godel are:
- Gödel's Proof by Nagel and Newman
- Forever Undecided by Smullyan
Some other nice resources on Godel are: