4 ms·

The perhaps surprising thing about theorem provers is that you do not use them to prove theorems. That is, you only use them on theorems you have already proven

The perhaps surprising thing about theorem provers is that you do not use them to prove theorems. That is, you only use them on theorems you have already proven, and the use is to persuade other people that your proof is valid. Otherwise I guess you would call it a "conjecture prover".

wetmore 4y ago
The proof is constructive though, so that's something.
- marcus_ 4y ago
  Not necessarily. Lean allows for axiom of choice.
andrepd 4y ago
Interactive theorem provers, perhaps, though I guess they also allow for exploratory use (though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true). But automated theorem provers (e.g. for first-order logic, SAT, or SMT), they can and have been used to solve open problems in mathematics: the famous four-color theorem, but many others.
- alimw 4y ago
  > though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true The Liquid Tensor Experiment [1] formalised a proof that the author himself found sufficiently complicated to have doubts about. And at a very different level, I myself began to formalise a proof [2] while it still had at least one hole in it. I was fortunate it turned out to be true! [1] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/ [2] https://github.com/agjftucker/exists-unique https://github.com/agjftucker/exists-unique
  - moloch-hai 4y ago
    If not, you could have published a proof that it was not. I knew somebody whose PhD project was a proof that all objects X are in Y. After rather some time he found instead that there are no objects X. That proof was not considered PhD material, although it seems like it should have been.
deterministic 4y ago
Theorem provers are used all the time to prove new things in computer science. A few examples: CompCert, SeL4 etc.

wetmore 4y ago

The proof is constructive though, so that's something.

marcus_ 4y ago
Not necessarily. Lean allows for axiom of choice.

andrepd 4y ago

Interactive theorem provers, perhaps, though I guess they also allow for exploratory use (though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true). But automated theorem provers (e.g. for first-order logic, SAT, or SMT), they can and have been used to solve open problems in mathematics: the famous four-color theorem, but many others.

alimw 4y ago
> though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true The Liquid Tensor Experiment [1] formalised a proof that the author himself found sufficiently complicated to have doubts about. And at a very different level, I myself began to formalise a proof [2] while it still had at least one hole in it. I was fortunate it turned out to be true! [1] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/ [2] https://github.com/agjftucker/exists-unique https://github.com/agjftucker/exists-unique
- moloch-hai 4y ago
  If not, you could have published a proof that it was not. I knew somebody whose PhD project was a proof that all objects X are in Y. After rather some time he found instead that there are no objects X. That proof was not considered PhD material, although it seems like it should have been.

deterministic 4y ago

Theorem provers are used all the time to prove new things in computer science. A few examples: CompCert, SeL4 etc.