About Mathematical Symbols in Proof General

Currently:

• ProofGeneralEmacs relies on X-Symbol
• ProofGeneralKit proposes PGML for simple symbol markup (cf HTML character entities)
• A future possibility is MathML

At the moment we consider PGML (or MathML) output would be produced by the theorem prover directly in its output display.

Since Proof General by design operates on proof scripts in their native language, there is no provision for generic input of mathematical notation. However, with the ProofGeneralCentralDocumentModel we may provide ways to map from mathematical notation into prover-input languages. This is the point to consider connecting to OpenMath and OMdoc.

TODO: add/discuss future plans here