Proof General is a generic interface for proof assistants, currently based on Emacs. It has been developed at the LFCS in the University of Edinburgh. Proof General works best under XEmacs, but can also be used with GNU Emacs. You need a recent version in either case.
The aim of the Proof General project is to provide powerful and configurable interfaces which help user-interaction with interactive proof assistants. The strategy of Proof General is to target power users rather than novices, building an environment for proof engineering. But we include modern user interface features, such as toolbar and menus, which make use easier for all. Proof General is currently used by many people for organizing large proof developments, and also for teaching interactive proof.
To read more about what Proof General provides, check the features list. To see what Proof General looks like in use, have a look at these screenshots. To download Proof General, visit the download page. To contact the developers, click .
Proof General comes ready-customized for these proof assistants:
| ","The Coq Home Page") ?> |
for
First crafted by
Healfdene Goguen.
Contributions by Patrick Loiseleur. Maintained by Pierre Courtieu. |
| ", "The Isabelle Home Page"); ?> | for
Crafted and maintained by
David Aspinall.
Additional maintainance, support for Isabelle/Isar by Markus Wenzel. |
| ", "The LEGO Home Page") ?> | for
First crafted by Thomas Kleymann
and
Dilip Sequeira.
Maintained by David Aspinall and Paul Callaghan. |
| for
Crafted and maintained by
Christophe Raffalli
and
Paul Roziere.
|
There are also experimental instances of Proof General:
These instances of Proof General are functional, but only show a bare fraction of what is possible. We are seeking volunteers to support and improve each of these (please send a note to if you're interested).
Proof General is ready to be customized to new proof assistants. It can be to get basic support working. Full documentation on configuration is provided.