Abstract

Arguably, the most crucial resource for scaling up mathematical proof to
the Internet age is the availability of machine-actionable libraries of
mathematical knowledge as well as information systems and semantic
services based on these libraries.

There are various mathematical knowledge collections and information
systems available. They range from completely informal ones like
Wikipedia or the Cornell arXiv, zbMath, and MathSciNet via mathematical
object databases like the GAP group libraries, the Online Encyclopedia
of Integer sequences (OEIS), and the L-functions and Modular Forms
Database (LMFDB) to theorem prover libraires like those of Mizar, Coq,
PVS, and the HOL systems.

Unfortunately, while all of these individually constitute steps into the
direction of research data, they attack the problem at different levels
(object, vs. document level) and direction (description- vs.
classification-based) and are mutually incompatible and
not-interlinked/aligned systematically.

I will survey methods and systems which can act as stepping stones
towards unifying these seeds into a Global Digital Library of
Mathematics. These methods and systems are inherently of flexible
formality (flexiformal) and range from heavyweight methods like
developing modular meta-logical formats for co-representing logics and
libraries in a common global meaning-space via all kinds of library
translations to lightweight methods for aligning and cross-linking such
libraries.

I will exemplify the methods on pragmatic examples (e.g. translating
LaTeX to HTML5 for arXiv.org importing PVS to OMDoc/MMT, or parsing the
OEIS) and discuss the infrastructures we need for managing a global,
flexiformal digital mathematical mathematical library.