MathLang: Experience-driven Development of a New Mathematical Language

AbstractIn this paper we report on the design of a new mathematical language and our method of designing it, driven by the encoding of mathematical texts. MathLang is intended to provide support for checking basic well-formedness of mathematical text without requiring the heavy and diffcult-to- use machinery of full type theory or other forms of full formalization. At the same time, it is intended to allow the addition of fuller formalization to a document as time and effort permits. MathLang is intended to, ultimately, be useful in providing better software support for authoring mathematics, reading mathematics, and organizing and distributing mathematics. The preliminary language presented in this paper is intended only for machine manipulation and for debugging of the design of MathLang