Talk:Hilbert program

mathematics free of intuition

"The vision of a mathematics free of intuition was at the core of the 19th century program known as the Arithmetization of analysis. " — At first, I got shocked: mathematics free of intuition?? It could fit computers, surely not humans! But after a minute I realized that what is really meant here, is "mathematics such that all proofs can (in principle) be formalized to the end, and then, their validity can (in principle) be checked with no help of intuition." Well, I understand that in some context this is habitually called "mathematics free of intuition". But maybe it is safer to note somewhere that outside this context, mathematics depends very heavily on intuition (still, and very probably, forever). Whoever disagrees, let him try to "explain" a proof to a "proof assistant" software (I did). For a short and simple proof this is as simple as a several-lines exercise in programming for beginners. But for a long and quite nontrivial proof this is as hard as a serious programming project. And no wonder: programming means, explaining simple ideas to an intuition-less monster. You explain, what is needed, to a programmer in 15 min, and then he/she explains the same to a computer in 3 months! This is the cost of no-intuition. Boris Tsirelson (talk) 21:47, 27 July 2015 (CEST)

Yes! Who ever actually does set theory work in a formal axiomatic environment? As you say, that's for proofs, which function like Wittgenstein's ladders: they are good for getting us to a higher level, but once we're up there, we don't need those ladders any more -- or do we?! --William Hayes (talk) 16:44, 29 July 2015 (CEST)