• ProofWeb is a web-based interface to interactive theorem provers run on a server. It is being enhanced towards a Wiki for formalized mathematics.
  • I3P is an IDE-based interface for Isabelle using Proof General-style interaction. It’s perhaps in a more robust state than our own Proof General Eclipse prototype.
  • As a possible foundation for generic proof environments, OpenMath is a standard representation form for mathematical objects, which links in with the MathML markup language.
  • Prosper was a project to develop an extensible, open proof tool architecture for incorporating formal verification into industrial CAD/CASE tool flows and design methodologies. The tools include novel user-friendly interfaces.
  • Isamode was an XEmacs front-end for Isabelle. It had a different feature collection compared with Proof General: script management wasn’t supported, but menus and shortcuts provided one of the first widely used enhanced interfaces for Isabelle.
  • CtCoq was an interface for the Coq theorem prover, developed at INRIA, Sophia Antipolis, as part of Projet CROAP. Like Proof General, CtCoq used a general approach for building user-interfaces for theorem provers. Unlike Proof General, CtCoq is based on a graphical environment with structure editing, created with the Centaur system.
  • OMEGA is a collection of web-based distributed tools for supporting theorem proving.