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

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

David Aspinall designed the web pages and graphics for Proof General.
Check the gallery for more publicity pictures!

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

Contact information

Have you any questions, comments, or suggestions about Proof General?
Send us a message using this form.

Discuss Proof General with other users and receive announcements by joining our mailing list.