Students of the course "Formal Methods and Specification" have an online application available that allows them to graphically prove formulas in the first-order predicate language, selecting proof rules by mouse clicks. The student will extend and improve this proof assistant in a way to be discussed with me.