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.
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
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.