Projects related to Proof General

Competition is healthy! Please add sections, notes and links below to describe related systems of interest for Proof General.

Matita

Omega

LeActiveMath

A teaching environment for web-based learning of mathematics.

TeXmacs

Visual document-based editor interface to computer algebra systems, using TeX fonts.

Has Coq interface tmCoq and Omega interface via the PLATO system

Theorema

See: http://www.risc.uni-linz.ac.at/research/theorema

Theorema is a prover built on top of the Mathematica system. It therefore has a nice interface, but is ''not'' freely available.