Add Mathlib as a source

[katjabercic]

Add Mathlib (Lean 4) as a source. A filtered subset of Mathlib definitions becomes candidate Items, linked to existing concepts via embedding-based alignment rather than shared identifiers.

Mathlib ships doc-gen output and a JSON declaration index. Confirm a stable URL/identifier per definition first. Possibly via leanprover-community/mathlib4 directly or the doc-gen artefacts.

Filtering: which definitions are concepts?

Most Mathlib definitions exist for formalization plumbing (helper lemmas, instances, internal constructions) and don't correspond to mathematical concepts as we mean them. We need a filter. Possible signals:

• Has a non-trivial docstring.
• Lives in a "main" namespace, not Tactic, Mathlib.Util, Mathlib.Init, etc.
• Referenced by many other definitions.
• Marked as a structure/class/inductive.
• LLM judge on (name + docstring): "is this a recognisable mathematical concept?"

Probably a combination. The filter itself is part of the work.

How aggressive should the filter be? False negatives (real concepts dropped) vs. false positives (plumbing imported as concepts).

Linking

Mathlib doesn't share identifiers with Wikidata etc., so Union-Find can't link it. Need embedding-based candidate links:

• Text embeddings of docstrings.
• Structural embeddings from the dependency graph.
• Combine both for alignment to existing concepts.

LLM voting ensemble can act as a second filter on candidate pairs.