4 ms·
"Bad at Calculating, Good at Everything Else" <- correct title IMHO It will be a long, long time until computers spit out something like the prove of Fermat's
by okket 9y ago
"Bad at Calculating, Good at Everything Else" <- correct title IMHO
It will be a long, long time until computers spit out something like the prove of Fermat's Last Theorem (which requires being good at math and not calculating).
- nothrabannosir 9y agoThen again, it was a long, long time until humans did, too.
- fooker 9y agoBtw, automated theorem proving is a thing and many non-trivial results have come from that field (i.e. theorems humans couldn't prove before).
- okket 9y agoIf this not only verification but generates genuine new proofs, then I might be wrong and have to remove one 'long'. Even then, I am convinced, it will still be a long time until computers can come up with such a complicated proof, involving so many different fields of mathematics, like Fermat's Last Theorem.
- mannykannot 9y agoFurthermore, math is not just about proving things. Mathematicians invent the consistent formalisms in which the process of proving takes place, and spot isomorphisms between apparently different ones. They also have a knack for choosing to follow paths that will be fruitful, rather than than lose themselves in a maze of pointless symbol manipulation. AFAIK, no computer has ever taken it upon itself to find a proof of some nontrivial issue in mathematics, let alone do any of the less formal things in mathematics.
- fooker 9y agoThe issue is that some (actually, most!) of the logics you can reason about are not decidable. So, it is hard to have a sense of progress towards a goal.