Definition/theorem ID service

[SReichelt]

In the library of the Slate theorem prover, definitions and theorems contain links to Wikipedia and other provers. On the one hand, this will not scale indefinitely, and on the other hand a web of such links could be useful on its own.

Idea

Offload the links to websites and theorem prover libraries to a separate "dictionary" service that is independent of Slate.

Motivation

• Fundamentally, the links are not really tied to the particular implementation of a definition or theorem in Slate/HLM, but rather to the definition/theorem itself. Slate should be just another theorem prover among others in the list.
• In a general form, maintaining such links could be useful beyond Slate, e.g. for navigating between arbitrary provers (to compare their implementation of the same concept), for comparing entire libraries, or even for searching within a specific library.
• In the long term, removing the links from Slate can reduce the maintenance cost of keeping them up to date (see below).
• Once the service has a sufficient amount of data and links to e.g. Wikipedia exist, we can hope for links in the reverse direction, e.g. from Wikipedia's info boxes.
• In particular, having links to Slate at a more general place can increase Slate's visibility. (Same for other provers, of course.)

Proposal

The idea is to make this a very lightweight service that merely provides the following:

• A unique ID for (potentially) every mathematical definition and theorem. Probably, everyone should have the ability to add a new item with minimal information, thereby generating a new ID.
• A list of links that are categorized in some way. A Wikipedia link should probably be mandatory for every item that has a Wikipedia entry, for two reasons:
  • When entering an item, this can be used to find out quickly if a similar item already exists, so that the user can extend the existing item instead.
  • A Wikipedia link is a good substitute for a description or even a name. (We may still want to give the user the option to provide an alternative name and description, though.)
• Perhaps some additional data like MSC classification.
• Relationships between items. This may become important e.g. when items are merged or split after people have started to rely on the unique IDs. May be extended over time, also with data from theorem prover libraries.

Conditions for success

Implementing the service described above only makes sense if more or less complete data for at least one other prover library (preferably more) is entered and also continuously maintained.
More specifically, considering the above description, the library contents of one or more provers must be enriched with Wikipedia links for all definitions and theorems where this is appropriate. The rest will happen automatically.

For this to be feasible, adding new entries must be as efficient as possible, ideally integrated into existing IDEs. (Integration into Slate is straightforward.)

Once this is done, it will hopefully create enough of an incentive to connect to it from other provers as well.

Maintenance

• At first, a simple periodic link check may be enough, as it is currently done for Slate/HLM.
• A more robust solution would be get such maintenance integrated into the build pipelines of the prover libraries that are referenced in the links. After refactoring parts of a library, the maintainers would be warned that some links need to be updated. Ideally, there should also be a check that new items are added to the service when appropriate.
• However, maintenance would become largely automatic if either the unique IDs or alternatively the Wikipedia links were simply referenced in the library source code. Of course, this would not exactly improve readability; however on the other hand it could become the basis of good IDE integration, e.g. by displaying additional information and providing tools for navigation and editing.

Related

• The closest equivalent is probably OEIS, the On-Line Encyclopedia of Integer Sequences. This obviously has a much narrower scope. A notable property of OEIS is that people generally refer to OEIS IDs whenever an integer sequence comes up.
• Regarding theorem provers, Freek Wiedijk's list of 100 theorems is basically a very limited version of this proposal.
• Fungrim provides stable IDs for some definitions and theorems (similarly to DLMF).
• MMT is also concerned with linking the libraries of different theorem provers, but the scope is much broader, also including translation. Potentially relevant: https://mathhub.info/library
• One could imagine this service to be integrated into e.g. ProofWiki or MathWorld. (However, existence of a ProofWiki or MathWorld entry should not be a requirement for adding a new item.)

[stub22]

I am quite interested in such shared libraries of term definitions.
Been studying recent work by Jacques Carette (@JacquesCarette at McMaster U), including collaboration with the @KWARC folks (who make MMT)

"Big Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge"
by Carette, Farmer, Kolhase, Rabe
https://www.researchgate.net/publication/346029333_Big_Math_and_the_One-Brain_Barrier_The_Tetrapod_Model_of_Mathematical_Knowledge (also avail on arxiv; not sure if that is exact same version)

...is supplemented by working notes here that contain some comparison tables across different math systems:
"The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems"
https://arxiv.org/abs/2002.04955

We may infer that the "Tetrapod" perspective is carried over into the agda-categories library:
https://github.com/agda/agda-categories
...which has a nice browsable HTML rendering here: https://agda.github.io/agda-categories/

Agda-Categories explanatory whitepaper includes table of comparisons across Agda, Coq, Lean, Isabelle libraries,
limited to the scope of categories described in the agda-categories library.
"Formalizing of Category Theory in Agda"
https://popl21.sigplan.org/details/CPP-2021/13/Formalizing-Category-Theory-in-Agda (includes link to arxiv preprint with the tables)

For comparison, here is the Lean MathLib source tree for category theory definitions:
https://github.com/leanprover-community/mathlib/tree/master/src/category_theory
...which can be seen in rendered-doc form here: https://leanprover-community.github.io/mathlib_docs/category_theory/category/default.html

Here is a discussion (2021-May) on the name-alignment topic in the Lean Zulip chat, regarding both MSC identifiers, and Wikipedia links.
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Using.20MSC.20identifiers.20in.20mathlib
@SReichelt linked to this "Idea" discussion in github from that Zulip chat topic, which is how I got here!

If there was already a well-liked shared namespace/ID approach, we might expect some of these folks to refer to it.
So I am guessing it does not quite exist yet, in the form we are discussing.
Perhaps we can collaborate in making it start to exist (in a usefully explicit form, in some workable scope).