The Gödelian insight has already been formalised
Programs have been developed that can derive Gödel's theorems. The Gödelian insight has, in effect, been formalised.
Penrose neglects this possibility because he fails to distinguish between the formal system within which a Gödel sentence is proven and the system that does the proving.

Stewart Russell and Peter Norvig (1995).

Note: This came was originally articulated as an attack on Penrose's response to Boolos—see "The Gödelian insight is all that we need", Box 66. Also, see the "Does Gödel's theorem  show that mathematical insight is not algorithmic?" arguments on this map.
CONTEXT(Help)
-
Artificial Intelligence »Artificial Intelligence
Are thinking computers mathematically possible? [7] »Are thinking computers mathematically possible? [7]
No: computers are limited by Gödel's theorems »No: computers are limited by Gödel's theorems
Improved machines »Improved machines
The Gödelian insight has already been formalised
Gödelization procedure algorithmically specifiable »Gödelization procedure algorithmically specifiable
SHUNYATA—implemented model »SHUNYATA—implemented model
+Comments (0)
+Citations (0)
+About