Very interesting work, I just looked at your paper. I like the idea of the proof cache which improves the individual user experience exploiting the collaborative setting; although I am not sure how this could be generalized to more general automation than the kind of term rewriting based search you describe.

Did you grade student derivations in a binary fashion, i.e. correct / incorrect, or did you also take into account especially "pretty" derivations or something like that?