Plato, the system for Interactive Mathematical Authoring built on top of Omega, looks good! Marc Wagner is the main developer. I am blogging this to remind myself that I have questions to ask.

Robert Lamar has the goal, which we also had in WebALT as a result of a requirement from our authors, "to restore natural language as a computerized mathematics input method" (paper in colour) - it looks very similar to our own approach - also syntax souring - (macro espansion in Lisp - LogiWEB): the way in which syntax nice for humans is made nice for computers too. Some of the souring operations remind me of those we are planning for evolving the mathematical grammar library: share, chain, fold, map, position. Annotation sounds like it is done by hand still however they have a system called ULTRA.

Technorati Tags: omega proof systems scientific text editor