Worked on something like this as a hobby project a while ago, but to avoid the complexities associated with solving arbitrary exercises, instead I had it set up as an algebra exercise generator: you start with the solution, which you then (algorithmically) obfuscate by splitting terms and recombining things for a couple of rounds. Never got around to finishing it, but the neat thing is that you've already generated one possible way to solve the problem, it's just how you generated the exercise in reverse.
Another thing that's quite easy to do is to check intermediate steps in a solution for equivalence. You don't even really need CAS, just brute force the problem by probing the equations: set all variables to randomly chosen values, n times and if the sets of results are the same for both equations, you're good.
Anyhow, Socratic looks great and a great deal more advanced and useful than what I came up with, so kudos!
Another thing that's quite easy to do is to check intermediate steps in a solution for equivalence. You don't even really need CAS, just brute force the problem by probing the equations: set all variables to randomly chosen values, n times and if the sets of results are the same for both equations, you're good.
Anyhow, Socratic looks great and a great deal more advanced and useful than what I came up with, so kudos!