I will discuss the integration of the authoring of a mathematical document and the formalisation of the mathematics contained in that document in a procedural proof assistant through the example of thecurrently in development integration between the Coq proof management system and the TeXmacs scientific editor. This software, tmEgg, turns TeXmacs into a new user interface to Coq.

TeXmacs allows the WYSIWYG authoring of scientific documents (at a level of abstraction similar to LaTeX) and is used as a user interface to several computer algebra systems, including the use of true mathematical notations (fractions, sigmas, integration symbols, indices, ...) instead of merely character strings.

Coq is a LCF-style (procedural) proof assistant; that is a proof assistant where one progresses in the proof by telling it what to do rather than what the intermediary steps in the proof are.

I'll present what tmEgg does differently than the usual Coq (and other proof assistants) user interfaces, how this is important in a document-oriented setting, what tmEgg does differently than the TeXmacs-CAS integration plugins and how this is important in the context of a proof assistant.