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

Information Retrieval from Mathematical Texts


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)