Knowls

Stream: LMFDB

[lmfdb-tunnel]

David Roe: We're planning on a few changes to the knowl infrastructure to help support this project:

• Currently we just use bold to indicate a definition in a knowl. We'd like to replace that with a jinja macro (maybe called DEFINES) that will allow us to include more semantic information as keyword arguments, such as an id for the definition (some knowls include multiple definitions), a link to the corresponding mathlib definition, a link to a wikidata id (for more general alignment purposes), and another knowl that explains how the LMFDB definition is related to those elsewhere (useful, for example, if the mathlib definition has been made in greater generality and looks superficially different).
• When formalizing definitions, it's often helpful to have theorems that use them; the LMFDB already has statements of many theorems and conjectures across the knowl database. We plan to add parallel macros (e.g. THEOREM and CONJECTURE) that can hold connections to mathlib and wikidata. It's a bit less clear to me how these should show up in the UI (we don't have a single term that can be bolded), but that question can be addressed a bit later.

[lmfdb-tunnel]

David Roe: The DEFINES macro is now live: there is documentation about its use here and you can see it in action here. In particular, you can now add links to mathlib by doing something like

DEFINES("group", mathlib="Algebra/Group/Defs.html#Group")

For THEOREM and CONJECTURE, I decided that these were already best supported by the existing \cites macro. I added all of the same external sites to this macro as are supported by DEFINES, so if you want to reference a mathlib theorem you can do something like

\cite{mathlib:Algebra/Group/Defs.html#inv_mul_cancel_comm}

Unfortunately, this doesn't currently work (because our hashtag pattern replacer replaces the second part of the url with an internal search link; this is resolved by #6728.

Next week I will work on updating the process for modifying the project blueprint from LMFDB knowls, but for now everyone should feel free to start adding mathlib links. Let me know if you have questions or need an account for editing LMFDB knowls.

[Chris Birkbeck]

This is great, thanks for this! I'll have a look later today and see if I can start getting some links added.

[Chris Birkbeck]

Ok I think I get how this works. But we'll need to wait until 6728 is done to get the links into the mathlib docs since they all use # at the end.

[lmfdb-tunnel]

David Roe: I think I have a slightly safer approach for #6728, but probably won't have time to do it until Wednesday.

[lmfdb-tunnel]

David Roe: I updated the PR, so it's just waiting for review now.

[lmfdb-tunnel]

David Roe: The PR is merged, so everyone is welcome to add links from LMFDB knowls to analogous Mathlib definitions. I've updated the README on our blueprint with instructions. Let me know if anything is unclear, or if you want an LMFDB account in order to help!