Organize your proofs!
Related Workshops and Conferences
Related Projects, Present and Past
ProofWeb is a web-based
interface to interactive theorem provers run on a server. It is
being enhanced towards a Wiki for formalized mathematics.
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,
is a standard representation form for mathematical objects, which
links in with the MathML
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
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.
was an interface for the Coq theorem prover, developed
at INRIA, Sophia Antipolis, as part of
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
a collection of web-based distributed tools for supporting
Web pages by
Please report issues
on PG trac.
Last modified 11 October 2013.