Formalizing Mathematical English


Language and Formalization of Mathematical English


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

Magdelena Wolska         Students’ language in computer-assisted tutoring of mathematical proofs” (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)

Marie Blanke                   Natural Language Processing of Mathematical Texts in mArachna

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

Parsing Mathematical Expressions

Deyan Ginev                    The Structure of Mathematical Expressions” (thesis)

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


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


Takuya Matsuzaki           “Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems”

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)