Novel Didactic Proof Assistant for First-Order Logic Natural Deduction

We present a proof assistant designed to help learning formal proof, particularly in the system of Natural Deduction for First-Order Logic. The assistant handles formulas and derivations containing meta-variables and allows to maintain a library of instanciable lemmas. It possesses a graphical interface presenting proofs as trees and handles multiple simultaneous derivations that can be dragged and dropped into one another.