(LML) Lean MathLib
treated as a library of math element types
(nLab) (nCatLab.org by Urs Schreiber et. al.),
treated as a structured, informal glossary of categorical math concepts.
Concept terms in the nLab vocabulary may be tried as query terms in an AxioMagic browser.
Builds on category theory and math formalization resources.
User models knit together background definition sources like Wikipedia, nLab, Lean/Agda libs in interactive knowledge views