> You could take a basic algebra problem as an example: 2x + 100 = 500. To solve this with brute force, we simply check every possible value of x until one works. We know, however, that it is far more efficient to rearrange the given equation using algebraic rules and in just two computations we get an answer.
I gave some thoughts about this lately, and it occurred to me that it's a problem that is similar to how computers play chess. I'd like to know if I'm right.
The equation 2x + 100 = 500 is an algebraic identity and with algebraic rules there is a finite number of ways to transform it. For instance, x + x + 100 = 500, 3x - x = 400, x + 200 = 600 - x, and so on. Each of these new equations can once again be transformed in a finite number of ways. So basically the initial equation is the root node of a tree that represents all the ways the equation can be transformed.
So it's a similar problem than for chess, or many other board games, where you start from a position and you must explore a tree of possibilities to find the leaves (checkmates, for instance). For an equation the leaves are nodes of the form x = numeric value.
Does that mean success in solving board games can have applications in computational math?
Sorry, this is just a trivial observation, but if you're going to accept
x + x + 100 = 500
and
3x - x = 400
you can probably list any variety along the lines of
(n)x - (n - 2)x + y = 400 + y
so clearly that isn't a finite transformation space.
Now, these transformations might look trivial, but this problem is too. So there's an interesting question of bounding your algebraic transformations to a subset of all possible transformations that still make all possible solutions available, which ultimately doesn't answer yours.
True, it is not finite. Still, considering the algorithm will not attempt to search the tree exhaustively anyway, maybe the fact that the tree is infinite does not make much difference.
PS. On second thought the number of rules is finite, so the number of possibilities has to be finite, at least if you apply the rules one at a time. It's the iteration of the rules that makes the tree infinite.
Nope, a single rule still has an infinite number of possibilities. As an example, multiplying both sides of the equation with an arbitrary constant produces a new valid equation, and there's an infinite number of constants to multiply with. (Bonus point: You get to choose what kind of infinity - countable or uncountable)
The reason a move tree[1] in a chess game has a finite number of nodes is not due to the finite number of possible transforms, but due to the fact that the number of possible board states is finite.
Yes, you can treat proof search as a game tree with "proof states" in the nodes and apply game playing heuristics to guide the search, eg. alphago style. From what I've read, these approaches do work, see for instance https://arxiv.org/abs/1701.06972. Nothing spectacular, but it's an improvement.
The fact that you are transforming a constant, into other constants, should be clear there is an infinite way to transform that. And so on. Also it is not similar in chess in that those equations that you derive from the starting one, are easily simplified back to the original one (or close to it).
I gave some thoughts about this lately, and it occurred to me that it's a problem that is similar to how computers play chess. I'd like to know if I'm right.
The equation 2x + 100 = 500 is an algebraic identity and with algebraic rules there is a finite number of ways to transform it. For instance, x + x + 100 = 500, 3x - x = 400, x + 200 = 600 - x, and so on. Each of these new equations can once again be transformed in a finite number of ways. So basically the initial equation is the root node of a tree that represents all the ways the equation can be transformed.
So it's a similar problem than for chess, or many other board games, where you start from a position and you must explore a tree of possibilities to find the leaves (checkmates, for instance). For an equation the leaves are nodes of the form x = numeric value.
Does that mean success in solving board games can have applications in computational math?