IMPS is an Interactive Mathematical Proof System intended to provide organizational and computational support for the traditional techniques of mathematical reasoning. It is

available under a BSD-like free license.

Mathematics Theorem Provers Application