Note: my main experience with theorem provers is with Type theory based proof-assistant, rather than an actual automated theorem prover.
It is obvious why naive automated theorem proving is inefficient: just doing an uninformed search through proof-space (e.g. with breadth first search) runs into the problem that the number of nodes in the proof tree increases exponentially with the number of steps.
What I am wondering is: Why haven’t we yet been able to create heuristics that guide an informed search to the point that automated theorem provers beat human mathematicians in proving theorems across the board? What makes it difficult to formulate such heuristics?