I used to feel the same way.
My dream was a computer that would give me the answers I wasn't able to reach because I wasn't smart enough.
Now I no longer hope that such a thing is possible; in fact, maybe I'm happy with it.
First: human reasoning works by "deepening", by "clarification"; a computer cannot see what is in your head, you have to explain it to it step by step; however, once you have succeeded, perhaps you no longer need the computer, because you have understood the subtleties of the problem and the problem disappears.
Second: in the automation of the game of chess there is a function that evaluates a configuration (heuristic) and a search algorithm based on this heuristic; if the heuristic were "exact", the search would no longer be needed.
In addition, if the heuristics are computationally heavy, the search cannot expand significantly, thus there is a tradeoff between accuracy and computation time. Neural network-based heuristics are computationally heavy, and those are the ones you're probably interested in. There are ATPs based on neural networks, e. g. Enigma (by Jan Jakubův). At the CASC-J10 Enigma performed very well, but did not win; Enigma relies on the "classic" theorem prover E (by Stephan Schulz), which is based on the equational superposition calculus and uses a variant of the Given-Clause Algorithm, the DISCOUNT Loop.
Regarding the possibility of having a "good" heuristic, I have thought of an argument that might convince you of the impossibility of its existence. I define a heuristic as "good" if it finds a proof of $n$ steps in at most $q(n)$ attempts, where $q$ is a polynomial and is known. If I had "good" heuristics, I could solve NP problems in polynomial time: suppose an NP problem has a verification algorithm in at most $p(n)$ steps ($p$ polynomial and known); in that case I can decide in polynomial time the NP problem, because I have answer YES if the heuristic finds a solution in less than $q(p(n))$ attempts and answer NO if the heuristic does not find a solution in less than $q(p(n))$ attempts (the composition of two polynomials is a polynomial).