Retrieval fixes: robust nprobe tuning + goals-only query

1. nprobe: set via faiss.extract_index_ivf() instead of attribute
assignment on the top-level index. FAISS silently ignores nprobe set
on wrapper indexes (IndexIDMap etc.), so reaching the IVF layer
directly guards against a future wrap making the tuning a no-op.
Verified the persisted index defaults to nprobe=16 and load bumps it
to 32. Non-IVF indexes and test doubles are tolerated (RuntimeError /
TypeError respectively) since search-breadth tuning must never break
index loading.

2. Retrieval query: goals only, newline-joined. Previously the retrieve
node space-joined goals + Lean error messages into one string. The
LeanDojo ByT5 encoder was trained on canonical proof states
("h : T\n⊢ goal"); error text is off-distribution noise that skews
the embedding. Errors still reach the LLM through the generation
prompt — they just no longer pollute retrieval. With no open goals
(pure syntax error) the query is empty and the retriever returns [],
which generation already handles.

Sanity check ("n : ℕ\n⊢ n + 0 = n"): top-5 = Nat.add_comm,
Nat.add_right_cancel, Nat.succ_add, Num.add_succ, Nat.add_assoc.
116/116 tests pass.

src/langgraph_agent.py

@@ -121,7 +121,13 @@ def make_verify_node(lean_env: LeanEnvironment):
 
 def make_retrieve_node(retriever: MathLibRetriever):
     def retrieve_node(state: ProofState) -> ProofState:
-        query = " ".join(state["goals"] + state["errors"])
+        # Query with goals only, newline-joined: the LeanDojo encoder was
+        # trained on canonical proof states ("h1 : T1\nh2 : T2\n⊢ goal"), so
+        # Lean error text is off-distribution noise in the embedding. Errors
+        # still reach the LLM via the generation prompt — just not retrieval.
+        # No open goals (e.g. pure syntax error) → empty query → retriever
+        # returns [] and generation proceeds without premises.
+        query = "\n\n".join(state["goals"])
         print("Retrieving relevant Mathlib lemmas…")
         lemmas = retriever.retrieve(query)
         print(f"  Retrieved {len(lemmas)} lemma(s).")

src/retriever.py

@@ -143,7 +143,13 @@ class MathLibRetriever:
         )
         # Tune IVFPQ search breadth. nprobe=32 / nlist=512 = 6% of clusters
         # searched — good recall/speed tradeoff for this index size.
+        # extract_index_ivf reaches the IVF layer even if the index is later
+        # wrapped (e.g. IndexIDMap); setting nprobe on a wrapper is silently
+        # ignored by FAISS, which this guards against.
+        import faiss
         try:
-            self._faiss_store.index.nprobe = self.nprobe
-        except AttributeError:
-            pass  # not an IVF index — nothing to tune
+            faiss.extract_index_ivf(self._faiss_store.index).nprobe = self.nprobe
+        except (RuntimeError, TypeError):
+            # RuntimeError: no IVF layer (e.g. flat index) — nothing to tune.
+            # TypeError: not a real faiss index (e.g. a test double).
+            pass