> How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathematical problems? I'm not sure how you could train it against

> How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathematical problems? I'm not sure how you could train it against itself. The branching factor would be infinite as well so I don't know how you'd constrain the legal moves. For example, maybe rewriting (a * 2) to (a + a) or (a * 4 - a * 2) and so on for every theorem you know would be useful in a proof, plus you can invent your own theorems as intermediate steps.