The only novel theorem I can recall being solved by a general artificial theorem prover is the Robbins conjecture. I’m sometimes surprised this area doesn’t attract more attention, since proving theorems is very similar to writing programs and automated program writers would be extremely useful.
automated program writers would be extremely useful.
I disagree. You have to specify the program that you want to write. Essentially, it means that you can use constraint programming instead of whatever other programming paradigm you’d use. I’m not convinced that that’s substantially easier.
Constraint programming would be extremely powerful. They aren’t a silver bullet, but they would make a ton of hard problems a lot easier. Particularly when it comes to proving whole-program correctness properties like “does not use more than X memory”.
For example, when a human programmer is designing a public key cryptosystem, they’re trying to satisfy properties like “there is no tractable Turing Machine that takes a public key as input and outputs the corresponding private key with non-negligible probability”. Doing that is really, really hard compared to just writing down what we want to satisfy.
It’s true that it would need to be insanely powerful. Even clever humans haven’t managed to prove that one-way hash functions exist (though we know a function that is one-way if and only if they exist...).
Note theorem proving is isomorphic to programming. Even if it wasn’t quite so equivalent, you could just ask for a constructive proof of a program satisfying whatever and the proof would contain the program.
The only novel theorem I can recall being solved by a general artificial theorem prover is the Robbins conjecture. I’m sometimes surprised this area doesn’t attract more attention, since proving theorems is very similar to writing programs and automated program writers would be extremely useful.
I disagree. You have to specify the program that you want to write. Essentially, it means that you can use constraint programming instead of whatever other programming paradigm you’d use. I’m not convinced that that’s substantially easier.
Constraint programming would be extremely powerful. They aren’t a silver bullet, but they would make a ton of hard problems a lot easier. Particularly when it comes to proving whole-program correctness properties like “does not use more than X memory”.
For example, when a human programmer is designing a public key cryptosystem, they’re trying to satisfy properties like “there is no tractable Turing Machine that takes a public key as input and outputs the corresponding private key with non-negligible probability”. Doing that is really, really hard compared to just writing down what we want to satisfy.
But that’s going to take an insanely powerful theorem-prover. Also, this is more the theorem-proving end than automated program end.
It’s true that it would need to be insanely powerful. Even clever humans haven’t managed to prove that one-way hash functions exist (though we know a function that is one-way if and only if they exist...).
Note theorem proving is isomorphic to programming. Even if it wasn’t quite so equivalent, you could just ask for a constructive proof of a program satisfying whatever and the proof would contain the program.