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. New icons for Proof General 4.4 were contributed by Yoshihiro Imai. For more on the history of the development of the Proof General program, see the preface and appendix of the user manual.
Contact information
Have you any suggestions, bug fixes or bug reports for Proof General?
Please browse the issues on GitHub
and add your own.
Receive announcements and ask questions about Proof General on our
low-frequency mailing lists for
users and
developers.