- **Agda-Unimath**: already imported. Curated, formal, but narrow in scope (univalent foundations). - **nLab**: already imported. Check it's scope (i.e. do they have articles on people or books). - **ProofWiki**: already imported. Check coverage. - **Others?** e.g. EoM, Wolfram MathWorld cross-links, Wikidata "same as" properties, Lean's Mathlib4 docstrings linking to Wikipedia.