3 ms·
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
by 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 agoIf 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.