3 ms·
I was going to say the same thing about SAT, or any NP-hard problem. The first example doesn't seem to be good either however. I don't think that proving a mat
by musicale 2y ago
I was going to say the same thing about SAT, or any NP-hard problem.
The first example doesn't seem to be good either however. I don't think that proving a mathematical conjecture which has resisted proof for decades (or longer) is something that we would typically expect a computer program to be able to do. Whenever this happens, it is hailed as a major breakthrough.
- anyfoo 2y agoIs there some circular logic in your reasoning? What is the difference between the computer program solving the conjecture, and “us” doing it?
- lmm 2y agoThe point is that it can complicate analysis of a program, at least if you take the fundamentalist view that all program behaviour should be provably correct. Like if you need the collantz sequence of a number or something in your program, you would just calculate it and use it, but it's surprisingly hard to prove that it always exists. Which isn't so much a problem in itself as it complicates trying to prove anything else about your program's behaviour.