Currently, there exists a big gap between formal computer-understandable mathematics and informal mathematics, as written by humans. When looking more closely, there are two important subproblems: making documents written by humans at least syntactically understandable for computers, and the formal verification of the actual mathematics in the documents. In our talk, we will focus on the first problem, by discussing some of the new semantic editing features which have been integrated in the GNU TeXmacs mathematical text editor.

To go short, the basic idea is that the user enters formulas in a visually oriented (whence user friendly) manner. In the background, we continuously run a packrat parser, which attempts to convert (potentially incomplete) formulas into content markup. As long as all formulas remain sufficiently correct, the editor can then both operate on a visual or semantic level, independently of the low-level representation being used. A related topic, which will also be discussed, is the automatic correction of syntax errors in existing mathematical documents. In particular, the syntax corrector that we have implemented enables us to upgrade existing documents and test our parsing grammar on various books and papers from different sources.

Occasion: MaGiX@Lix, Palaiseau, September 23, 2011

Documents: slideshow, TeXmacs source