My girlfriend and I are starting to play around with proof assistants (avoiding the coq joke as best I can...) and it would be great to have something like this to go along with that endeavour.