The Last Question
Can a user-friendly computer proof assistant satisfy the mathematician’s desire for certainty without killing the pleasure?
To arrive at the edge of the world's knowledge, seek out the most complex and sophisticated minds, put them in a room together, and have them ask each other the questions they are asking themselves.
Can a user-friendly computer proof assistant satisfy the mathematician’s desire for certainty without killing the pleasure?