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