Semantic representation of mathematics

Or, knowledge representation for mathematics. Applications include proof assistants and automated theorem provers. Related to the foundations of mathematics.

Community activity

2016 Fields Institute Workshop on Semantic Representation of Mathematical Knowledge :
- Documentary-style summary video and talks
- Good talks by
  - Jeremy Avigad (slides 1 ,2 ), a developer of the Lean theorem prover
Sessions at ICMS 2018 (doi):
- Session 8 : Machine learning for mathematical software
- Session 19 : Formal and informal mathematical corpora

Standards

Mathematical Markup Language (MathML)
- Two flavors: Presentation and Content
- Hodson, 2014: Ry’s MathML Tutorial (epub ) (only Presentation MathML)
- Barnhart: Connexions Guide to MathML, Sec 3: Content MathML (epub )
OpenMath
- Technical overview
- Comparison with MathML
  - MathML is for presentation, OpenMath is for semantics
  - For high-school level math, both Content MathML and OpenMath work
  - For more advanced math, only OpenMath defines semantics
- Dalmas et al, 1997: An OpenMath 1.0 Implementation (doi, pdf)
- Buswell et al, 2004: The OpenMath 2.0 Standard (pdf)
OMDoc : Open Mathematical Documents
- Container for MathML and OpenMath
- Extends OpenMath from expressions to also statements and theories
- Kohlhase, 2006: /OMDoc 1.2 Book /(pdf)

Libraries

MO has a big list of “atlas-like websites” for specific areas of mathematics.

Digital Library of Mathematical Functions (DLMF)
- Miller & Youssef, 2003: Technical aspects of the DLMF (doi)
Digital Repository of Mathematical Formulae (DRMF)
- Cohl et al, 2014: DRMF (doi, arxiv)
- Cohl et al, 2015: Growing the DRMF with generic LaTeX sources (doi, arxiv)
Global Digital Mathematics Library (GDML)
- NRC, 2014: Developing a 21st century global library for mathematics research (doi, arxiv)
- Olver, 2012: What’s happening with the World Digital Mathematics Library? (slides)
- Present status of project is unclear; possibly vaporware
Mathematical Functions Grimoire (FunGrim) (GitHub )
- Similar in scope to DLMF but fully open and greater emphasis on semantics
- Johansson, 2020: FunGrim: a symbolic library for special functions (arxiv)

General

Carette, Farmer, Kohlhase, Rabe, 2019: Big math and the one-brain barrier: A position paper and architecture proposal (arxiv)

Semantic Web

Lange, 2013: Ontologies and languages for representing mathematical knowledge on the Semantic Web (doi, pdf)
Bröcheler, 2007: A mathematical semantic web (pdf)

Recognizing and parsing mathematical expressions

Zanibbi & Blostein, 2012: Recognition and retrieval of mathematical expressions (doi)
Chan & Yeung, 2000: Mathematical expression recognition: a survey (doi)

Parsing LaTeX:

Parsing PostScript and PDF:

Yang & Fateman, 2003: Extracting mathematical expressions from PS documents (pdf)