Name: Anonymous 2014-06-01 20:28
Gödel didn't need a proof assistant, why do you? You'll never succeed in making maths entirely computable, automatable, never.
In the manuscript La Clef des Songes he explains how considering the source of dreams led him to conclude that God exists.[25] His growing preoccupation with spiritual matters was also evident in a letter entitled Lettre de la Bonne Nouvelle that he sent to 250 friends in January 1990. In it, he described his encounters with a deity and announced that a "New Age" would commence on 14 October 1996.