Preserving meaning in a database
A database can store a polynomial as a list of integers. That storage type does not say which coefficient comes first, which ring the polynomial belongs to, or what a computed root means. The MathDataHub work addresses this gap between mathematical objects and their encodings.
Berčič, Kohlhase, and Rabe describe MDDL, a language for mathematical data schemas, and MBGen, which generates database and interface infrastructure from them. The schemas use MMT theories; codecs connect mathematical types to concrete encodings. The author-hosted manuscript reports this construction and dataset applications.
Provenance as a system responsibility
The manuscript’s concluding discussion proposes provenance at the level of datasets, properties, and individual results, available through interfaces and queries. It also considers when to cache a value and when to recompute it. These are proposed extensions in that account. They should not be presented as a completed general provenance service.
An algebraic value and its evidence
Suppose a computation returns an algebraic root. The encoded value, the polynomial it belongs to, and the certificate establishing its properties have different roles. A downstream computation needs both an interpretable value and evidence appropriate to the claim it uses. A record that says where the value came from helps inspection; a checker must still establish the claimed property.
The comparison with Axeyum
Axeyum records formal statements, evidence, proof routes, and dependencies. Its constructive analysis examples also distinguish approximate existence from exact values. MathDataHub supplies a related design lesson: preserve mathematical meaning across storage and computation, rather than expecting an identifier or serialized value to carry that meaning alone.
For Axeyum, a reusable computation cache should bind its inputs and checker identity to the returned artifact. A change to the input polynomial must not silently reuse an old root certificate. Connecting those checks to task selection is a concrete development goal; the broad idea of mathematical provenance already has a research history.
OpenDreamKit and MMT/MathHub supply the wider interoperability context.