You start with the axioms, and each turn you perform one of a small set of well defined moves. You win if you get to a certain statement. I don’t see any fundamental difference from a game (though admittedly we don’t know whether winning is possible if the theorem hasn’t been proven yet).
In particular, generalized chess (chess on an NxN board, with an appropriate number of pieces) is EXPTIME-complete: for any instance of a binary decision problem in EXPTIME, you can reduce it to a generalized chess board position such that the White (Black) player can win iff the answer to the instance of the decision problem is Yes.
The complexity of theorem proving depends on the formal system. There are some logics where theorem proving is PSPACE-complete, which is contained in EXPTIME. Other interesting logics are undecidable, thus you can’t reduce them to a game of generalized chess, although semidecidable logics can be reduced to other, more complex games.
You start with the axioms, and each turn you perform one of a small set of well defined moves. You win if you get to a certain statement. I don’t see any fundamental difference from a game (though admittedly we don’t know whether winning is possible if the theorem hasn’t been proven yet).
That works for finitely axiomatized theories. If you have axiom schemas as in standard ZF(C) or PA then there is no small set of well defined moves.
The axiom schemas are countable, which is small enough for the procedure described in the grandparent to work. Unless I’m not understanding something?
The size of the search space and lack of any reasonable heuristic.
Yes.
In particular, generalized chess (chess on an NxN board, with an appropriate number of pieces) is EXPTIME-complete: for any instance of a binary decision problem in EXPTIME, you can reduce it to a generalized chess board position such that the White (Black) player can win iff the answer to the instance of the decision problem is Yes.
The complexity of theorem proving depends on the formal system. There are some logics where theorem proving is PSPACE-complete, which is contained in EXPTIME.
Other interesting logics are undecidable, thus you can’t reduce them to a game of generalized chess, although semidecidable logics can be reduced to other, more complex games.