Formalizing Mathematical English


Language and Formalization of Mathematical English


Marcos Cramer               “Proof-checking mathematical texts in controlled natural language” (dissertation)

Muhammad Humayoun              “Developing the System MathNat for Automatic Formalization of Mathematical Texts (dissertation)

Mohan Ganesalingam   “The Language of Mathematics” (dissertation)

Andrei Paskevich            “Methods of formalization of mathematical knowledge and reasoning” (dissertation)

Clauss Zinn                       “Understanding Informal Mathematical Proofs” (dissertation)

Donald Simon                  "Checking Number Theory Proofs in Natural Language" (dissertation)

Aarne Ranta                     “Type Theory and the Informal Language of Mathematics”

Kay O’Halloran                Mathematical Discourse: Language, Symbolism, and Visual Images (Book)

Charles Wells                   A Handbook of Mathematical Discourse (Book)

Zinaida Trybulec             Some Remarks on The Language of Mathematical Texts

Manfred Kerber              Informal and Formal Representations in Mathematics

Candia Morgan               The Language of Mathematics”: Towards a Critical Analysis of Mathematics Texts

Topics in Mathematical Knowledge Management


Steve Keiffer                    “A Language for Mathematical Knowledge Management” (thesis)

Stefan Anca                      Natural Language and Mathematical Processing for Applicable Theorem Search” (thesis)

Deyan Ginev                    The Structure of Mathematical Expressions” (thesis)

Mihai Grigore                  Knowledge-poor Interpretation of Mathematical Expressions in Context” (thesis)

Magdelena Wolska        “A Language Engineering Architecture for Processing Informal Mathematical Discourse”

Marie Blanke                   Natural Language Processing of Mathematical Texts in mArachna

Sabina Jeschke                “Information extraction from mathematical texts by means of natural language processing techniques”

Research Groups Focusing on Aspects of Formalizing Mathematical Language


Laboratory for Text Content and Media (Aizawa Lab)

Knowledge Adaptation and Reasoning for Content Group (KWARC)

The Language and Mathematics Processing and Understanding Group (LaMaPUn)

Natural Language Proof Checking (Naproche)

The System for Automated Deduction (ForTheL , Evidence Algorithm)



Discourse Representation Theory


Hans Kamp                       From Discourse to Logic: Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory (Book)

Hans Kamp                       Handbook of Philosophical Logic: Volume 15, “Discourse Representation Theory”. Dec 2010. p 125 – 395.

Patrick Blackburn            Working with Discourse Representation Theory (Book)

Uwe Weyle                       Discourse Representation Theory (Book)

Relation Algebras and Natural Language


Michael Bottner              Peirce Grammar

                                           Relational Grammar (Book from dissertation)

Renate Schmidt               “Terminological Representation, Natural Language & Relation Algebra”

                                           “Relational Grammars for Knowledge Representation”

Patrick Suppes                 Elimination of quantifiers in the semantics of natural language by use of extended relation algebras

Uta Priss                           An application of relation algebra to lexical databases

Markup Languages for Content of Mathematics








Conferences on Intelligent Computer Mathematics (CICM)

NTCIR-11 Task: Math-2 (Math Retrieval)

Tenth International Conference on Mathematical Knowledge Management

European Summer School in Logic, Language, and Information

Related Work


Andrew Aberdein           The Argument of Mathematics (Book)

Edwin Coleman               “The Role of Notation in Mathematics” (thesis)

Florian Cajori                   A History of Mathematical Notations vol I & II (Book)

Steven Schwartzman     The Words of Mathematics: An Etymological Dictionary of Mathematical Terms used in English (Book)

Richard Epstein               Predicate Logic: The Semantic Foundations of Logic (Book)

ACE                                    Attempto Controlled English

Proof Wiki                        ‘The online compendium of mathematical proofs’


Formalized Mathematics


IsarMathLib                     ‘A library of formalized mathematics for Isabelle/ZF theorem proving environment’

Mizar                                 Journal of Formalized Mathematics

Coq Proof Assistant        The Coq Standard Library

MetaMath                        Metamath Proof Explorer


Partially Formalized Mathematics Texts


A Compendium of Continuous Lattices (in Mizar)

Grundlagen der Analysis by Landau (in Naproche)

Axiomatic Set Theory by Suppes (definitions in Keiffer’s MS thesis in DZFC and by Friedman in ‘Proofless Text’ )

Topology by Munkres (definitions in Keiffer’s MS thesis in DZFC)


Euclid’s Elements (in early stages in Naproche)

Elementary Theory of Numbers by LeVeque (several proofs in Simon’s Nth Checker)

An Introduction to the Theory of Numbers by Hardy and Wright (a few proofs in Zinn’s VIP)