Injecting Formal Mathematics Into LaTeX

The paper presents the format for representing informal mathematics. acts as a surface language for two systems: the (presentation-oriented) system to produce PDF  and the semantics-aware  system for advanced knowledge management services. We discuss how the markup facilities allow in situ flexiformalization (and the necessary elaboration of complex structures), while staying presentationally neutral.