Hmm, yeah, you are right. Rybka, Deep Fritz and their predecessors look like a smaller effort than ATPs, actually. And other chess programs are at about the same level (and close to the top human players’ level, apparently?). Both areas look from outside like good targets for narrow AI , but apparently there is something about theorem proving that requires some poorly formalized part of human reasoning.
Human chess also involves loads of poorly formalized reasoning, but chess is a vastly smaller search space. There is no game you can play which gets you to Fermat’s Last Theorem.
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.
Mostly they teach various theorems and their proofs, so that you can “stand on the shoulders of giants”, and they try to train your “intuition” (incommunicable heuristics) by exercise in proving simple theorems.
More advanced math courses teach explicit heuristics (in the form of “proof strategies”: general patterns that are often found in proofs), which can be programmed in an automated theorem prover to some extent, but they are not good enough to make up for the lack of human-level intuition.
On the other hand we know excellent heuristics for chess, in the form of position evaluation functions that give an higher score to positions which are more likely to lead to a victory. The chess piece relative value heuristic, for instance, is extremely simple and yet very effective. High-level computer chess programs use much more complicated evaluation functions, but chess piece relative value is usually the dominant component of it.
If theorem proving was as popular as chess, some Deep Blue MathRybka program would have solved a Millennium problem by now.
I suspect you are factually mistaken and would expect to find more resources going into theorem-proving.
Hmm, yeah, you are right. Rybka, Deep Fritz and their predecessors look like a smaller effort than ATPs, actually. And other chess programs are at about the same level (and close to the top human players’ level, apparently?). Both areas look from outside like good targets for narrow AI , but apparently there is something about theorem proving that requires some poorly formalized part of human reasoning.
Human chess also involves loads of poorly formalized reasoning, but chess is a vastly smaller search space. There is no game you can play which gets you to Fermat’s Last Theorem.
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.
We know very good heuristics for chess, that’s not the case for general theorem proving.
Then what do high school geometry instructors teach?
Mostly they teach various theorems and their proofs, so that you can “stand on the shoulders of giants”, and they try to train your “intuition” (incommunicable heuristics) by exercise in proving simple theorems.
More advanced math courses teach explicit heuristics (in the form of “proof strategies”: general patterns that are often found in proofs), which can be programmed in an automated theorem prover to some extent, but they are not good enough to make up for the lack of human-level intuition.
On the other hand we know excellent heuristics for chess, in the form of position evaluation functions that give an higher score to positions which are more likely to lead to a victory. The chess piece relative value heuristic, for instance, is extremely simple and yet very effective. High-level computer chess programs use much more complicated evaluation functions, but chess piece relative value is usually the dominant component of it.
Also, high school geometry is much simpler than mathematics in general, and there are good automatic theorem provers for geometry.