4 ms·
That's simply not true. The kinds of statements that are unprovable aren't "intuitive". Gödel provided an algorithm for creating them!
by sukilot 6y ago
That's simply not true. The kinds of statements that are unprovable aren't "intuitive". Gödel provided an algorithm for creating them!
- __MatrixMan__ 6y agoBut there's no reason to believe that his algorithm gives us all of them. Nobody has proven, for instance, that the Goldbach conjecture is unprovable, but the collective intuition of the community of number theorists is such that nobody spends much time trying to prove it anymore. What, aside from some coded-in GIT awareness-would lead an automated prover to do the same?
- tialaramex 6y agoWhy can't an automated prover have intuition? Today's automated provers don't, but then not so many years ago the successful computer chess players were all these boring rules-based brute force engines. And then DeepMind showed that a very different approach is better.