PIMS-ULethbridge PIMS Distinguished Visitor Series: Fairouz Kamareddine

Mathematical texts can be computerised in many ways. At one end there is document imaging, at the other there are proof assistants (Mizar, Isabelle, Coq, etc.).In between, there are typesetting (e.g., LaTeX and MathML) and semantically oriented (e.g., OpenMath and OMDoc) systems. MathLang is an approach for computerising mathematical texts which is flexible enough to connect the different approaches to computerisation, allowing various degrees of formalisation and compatibility with different logical frameworks (set/cate­gory/type theory) and proof systems.

MathLang adds, checks, and displays various information aspects on mathematical texts. One aspect is a weak type system that assigns categories (term, statement, noun, adjective, etc.) to parts of the text, and checks that grammatical sense is maintained. Another aspect allows identifying chunks of text, marking their roles (theorem, definition, explanation, example, section, etc.), and indicating relation­ships between the chunks (A contradicts B, A follows from B, etc.). Further aspects allow additional formality such as proof structure and details of how a human-readable proof is encoded into a fully formalised version of Mizar/Isabelle/Coq. In this talk we survey the status of the MathLang project.