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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.