Waterproof: Educational Software for Learning How to Write Mathematical Proofs

From the abstract:

> Waterproof is based on the Coq proof assistant. As students type out their proofs in the program, it checks the logical soundness of each proof step and provides additional guiding feedback. Contrary to Coq proofs, proofs written in Waterproof are similar in style to handwritten ones: proof steps are denoted using controlled natural language, the structure of proofs is made explicit by enforced signposting, and chains of inequalities can be used to prove larger estimates.

I had been looking for something like this to play around with interactive theorem proving! Thanks.