4 ms·
I think 10 years probably won't cut it for a computer proving big new theorems in math. A likely step by step evolution may be: 1) Verification of non-algorit
by thomasahle 10y ago
I think 10 years probably won't cut it for a computer proving big new theorems in math.
A likely step by step evolution may be:
1) Verification of non-algoritmic programs: Everything is specified reasonably well.
2) Verification of mathematical proofs. This shouldn't be hard in principle, but it does require very good natural language understanding and the ability to prove partial results.
3) General proving as good as humans. We have still to see any non-trivial results in this direction at all.
- ScottBurson 10y agoFor verified software, we probably don't need many big new theorems. We probably just need to be able to apply a large library of well-known strategies to a mind-numbingly long list of routine proof obligations. It's more about exhaustive case analysis, which computers are good at, than about creative leaps of intuition. The big problem, IMO, is search control: keeping the computer from wandering off into parts of the search space that don't actually matter.
- kmicklas 10y agoWhy is 2) relevant? Natural language understanding is way harder and a totally unrelated problem.
- sanxiyn 10y ago2 is relevant because there exists vast amount of mathematical proofs already written in natural languages. It's about supporting legacy code.