> 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/ [2] https://github.com/agjftucker/exists-unique