Since I have been reading Goedel, Escher, Bach many years ago, the question, what (if anything) Goedel's theorem has to say about the relation between human intelligence and AI has been working in the back of my mind. Later my thinking was influenced by reading the books of Roger Penrose (eg. The Emperor's New Mind). I always found Penrose's argument for the superior power of our human mind compared to computer algorithms very convincing. For example, he argues, that every child can understand the concept of natural numbers, whereas the Peano axioms and any extension can not distinguish them from supernatural numbers. On the other hand, formalists like to make the case of how strictly formalizing geometry helped to solve the centuries lasting struggle with the parallel axiom and resulted in the birth of the fruitful mathematical field of non Euclidian geometry. In their view, this example shows, how intution can be fooled and thus is not per se superior to formal systems. A vague idea I have on this, is, that maybe the reason, why very smart people on "plantonist" and "formalist" sides can not agree on a common standpoint on this, might be, that the question is not well posed in the current form. I think, whenever we try to compare the power of the intuitive concept of truth with the formal concept of formal provableness, we are lacking a third independent concept, which could act as a referee between the two. How could intution ever be recognized to be superior to a formal system, when all what we allow as a referee, is a proove in a formal system. If you are able to read German, here is a very nice link: http://www.joergresag.privat.t-online.de/ Especially reading chapter 4.4 of "Die Grenzen der Berechenbarkeit" has given me the stong feeling, that the appearance of supernatural numbers out of the Peano axioms is to be regarded as resulting from a limitation of the concept of formal systems and is not due to the "fuzziness" of the the intuitive concept of natural numbers (unlike in the case of geometry). But how can you make the case, if all you have, is formal systems and our "fuzzy intution"?