mathlib-lookup

mathlib-lookup

This skill exists for the user's single stated pain point: they know the mathematics and not the Mathlib name. Two consequences govern everything below.

1. A name is a claim, and claims get checked. Nothing unverified is ever reported, used, or written - not even hedged with "I think". A hedge disappears the moment the name is repeated.
2. A name alone is not an answer. Report the real elaborated type. The user needs the hypotheses and their order to use the lemma; the name is only the handle.

Repository root: /path/to/lean-interact.

---

The escalation, in order of cost

Stop at the first step that yields a verified name.

1. Dot completion (free, when a hypothesis exists)

If the user has h : Nat.Coprime a b in context, the whole Nat.Coprime namespace is reachable as h.something, and the editor's completion list is guaranteed correct for this Mathlib. Tell the user to type h. in the VS Code infoview pane. The programmatic equivalent is step 2's --namespace.

2. Guess from the naming grammar (seconds)

Read vault/Naming Conventions.md. Construct the name rather than recall it:

• Say the statement in Mathlib's vocabulary: "modEq iff dvd", "le of dvd", "prime dvd mul".
• Conclusion first, hypotheses after of_; symbols become fragments (+ -> add, ∣ -> dvd, ↔ -> iff, ≤ -> le, ^ -> pow, % -> mod/emod).
• Namespace = the type of the distinguished hypothesis, or the head of the conclusion.
• Casing migration: natCast not nat_cast, intCast not int_cast. Pre-2024 sources and mathlib3 names are systematically wrong.
• Always try the primed variant too; ' means different hypotheses or argument order (Nat.modEq_iff_dvd vs Nat.modEq_iff_dvd').

Then verify (step 4). A guess that verifies costs one command.

3. Search with tools/mlq.py (seconds)

python3 tools/mlq.py "modEq iff dvd"          # free text over names and statements
python3 tools/mlq.py --about "chinese remainder"   # by informal topic
python3 tools/mlq.py --concept ModEq          # by the concept appearing in the statement
python3 tools/mlq.py --namespace Nat.Prime    # the whole API of a namespace or type
python3 tools/mlq.py --help                   # authoritative; the tool wins over this note