Proof General is a generic interface for proof assistants, currently based on the customizable text editor Emacs. It works with either XEmacs or GNU Emacs. Proof General has been developed at the LFCS in the University of Edinburgh.
To find out more, check the features list and look at the screenshots. To get Proof General, visit the download page. If you're not interested in interactive proof, see the standalone components developed as part of Proof General. To contact the developers, click .
Proof General comes ready-to-go for these proof assistants:
| ", "The Isabelle Home Page"); ?> | for
By
David Aspinall
and
Markus Wenzel.
|
| ","The Coq Home Page") ?> |
for
By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
Pierre Courtieu.
|
| ", "The PhoX Home Page") ?> | for
By
Christophe Raffalli
and
Paul Roziere.
|
| ", "The LEGO Home Page") ?> | for
By Thomas Kleymann, Dilip Sequeira,
David Aspinall
and
Paul Callaghan.
|
There are also experimental or in-development instances of Proof General:
The instances of Proof General marked "in development" above are not considered complete, but are supported by the developers of proof systems. The other instances above are "technology demonstrations" of Proof General for other popular provers, 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.