Penrose - Gödel - AI
A formal system (such as a computer program) can not prove all true statements. Roger Penrose is among those who claim that Gödel’s theorem limits what machines can do. (Wikipedia)
Beyond the Doubting of a ShadowA Reply to Commentaries on Shadows of the Mind
