Organize your proofs!  Home  Features  Download  Documentation  About  News  Screenshots  Development  Publications  Related

About the Proof General project

The forefather of Proof General was LEGO mode, begun in 1994 at the LFCS by Thomas Kleymann. LEGO mode was an Emacs-based front end for LEGO similar to David Aspinall's Isamode, developed at the LFCS since 1992. After 1994, implementations of proof-by-pointing and script management were added to LEGO mode, and the code was made generic. The generic basis was developed by Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall. The current authors and maintainers of the various instantiations of Proof General are mentioned on the front page and in the AUTHORS file.

The Proof General project was coordinated until October 1998 by Thomas Kleymann, and since then by David Aspinall. The project has benefited from travel and auxiliary support funding by EPSRC, the EC, and the LFCS.

David Aspinall designed the web pages and graphics for Proof General.

For more on the history of the development of the Proof General program, see the manual appendix.

Contact information

Have you any suggestions, bug fixes or bug reports for Proof General?
Please visit the Trac pages to browse tickets and add your own.
Receive announcements and ask questions about Proof General on our low-frequency mailing lists for users and developers.