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 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-customized 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 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.