The potentially interesting thing here, to me, is using networks to short-circuit searches that could grow explosively with expression size, but then filter dow

The potentially interesting thing here, to me, is using networks to short-circuit searches that could grow explosively with expression size, but then filter down to answers that can be shown correct. That's also a way to get some value out of a system that doesn't always produce the correct answer as its first guess. In some cases it may be easy to prove the correctness once you have the proposed answer, but in others the network might need to produce intermediate steps or some kind of 'argument' to let the CAS check correctness in reasonable time. Perhaps do that by instrumenting a CAS to output intermediate steps and train the network on that, not just problem/answer pairs. Broadly, humans who have seen a lot of problems solved can say "this looks like a situation where you could try X" and do X without going down all the blind alleys that a CAS might. So it doesn't seem implausible that automated learned models might also outperform the heuristics CASes have hard-coded in for making those kinds of guesses. (You can imagine closer coupling, e.g. a CAS that calls out to an NN to propose solutions to certain hard-to-solve-but-easy-to-check subproblems, or uses learned models to try to guess the right branch to go down in a solution process that already looks like searching a tree of possibilities. But the more you have to crack open the CAS, the less appealing the whole thing becomes.)