OEIS importer and extension for MathDataHub
MathDataHub (MDH) is a deep FAIR system for mathematical data sets. Currently, it has mostly been used for systematic data sets like the Small Groups Library. Having the OEIS (Encyclopedia of Integer Sequences) in MathDataHub would be a major undertaking and a major success. Some of this we have already done, see E. Luzhnica and M. Kohlhase (2016) Formula semantification and automated relation finding in the OEIS. ICMS 2016. This needs to be made sustainable and much more complete. MathDataHub and MathHub are the right tools/targets for this. We have to
- get our hands on the OEIS dumps - KWARC has the necessary contacts - and build an infrastructure to keep the content synced.
- build a parser for the OEIS that is as lossless as possible
- formalize the meta-theory of OEIS in MMT.
- Build the MDDL Schema theories for the OEIS
- (optionally) Build specialized User Interfaces on top of MDH.
- (optionally) build a programmatic API for the OEIS.
Clearly this is a project for a whole group, and the later points are optional.