>One way of describing the Incompleteness Theorems (1931) of the Austrian logician Kurt Gödel is to say that he proved, in the form of a mathematical theorem, that the possibility of a fully automated mathematics can never be realized.
Which suggests the following solution : limit our endeavors to that part of mathematics that CAN be automatically proven (and drill down infinitely into details thereof). And stub off the rest with good-enough axioms (aka holy doctrine).
Crazytalk? Well it's basically how we as a culture handle pretty much everything, epistemologically (and ontologically) speaking.
It could be very efficient. It could be a dystopian nightmare.
Which suggests the following solution : limit our endeavors to that part of mathematics that CAN be automatically proven (and drill down infinitely into details thereof). And stub off the rest with good-enough axioms (aka holy doctrine).
Crazytalk? Well it's basically how we as a culture handle pretty much everything, epistemologically (and ontologically) speaking.
It could be very efficient. It could be a dystopian nightmare.