Upload folder using huggingface_hub

ragsolver/agents/agents.py

@@ -0,0 +1,209 @@
+"""Agentes (Rol A) — Planificador, Generador, Autoformalizador, Crítico y las dos
+líneas base de la propuesta §8.2. Cada uno: arma un prompt (configs/agents.yaml),
+hace UNA llamada LLM con salida JSON validada por Pydantic y devuelve el modelo.
+
+El contexto de recuperación llega ya formateado (docs/PLAN_RAG.md Fase 4, tarea 4):
+lemas como `[M1] name : signature — description (module)`; ejemplares como
+`[I1] statement — key idea — source, page`.
+"""
+
+from __future__ import annotations
+
+import json
+import re
+import textwrap
+import time
+
+import yaml
+
+from ragsolver.agents.schemas import BaselineAOutput, BaselineBOutput, CriticOutput, FillOutput, FormalizerOutput, GeneratorOutput, PlannerOutput, Problem
+from ragsolver.llm import LLM, LLMResponse
+from ragsolver.logging.jsonl_writer import append_event
+from ragsolver.rag.retrieve import mathlib_table_name
+from ragsolver.rag.schema import Hit, TraceEvent, VersionsPin
+
+
+def load_agents_config(path: str = "configs/agents.yaml") -> dict:
+    return yaml.safe_load(open(path, encoding="utf-8"))
+
+
+def format_lemmas(hits: list[Hit]) -> str:
+    lines = []
+    for h in hits:
+        m = h.metadata
+        desc = (m.get("informal_description") or "")[:300].replace("\n", " ")
+        line = f"[{h.citation.citation_id}] {m.get('decl_name')} : {(m.get('signature') or '')[:400]}"
+        lines.append(line + (f" — {desc}" if desc else "") + (f" ({m.get('module_path')})" if m.get("module_path") else ""))
+    return "\n".join(lines) or "(none)"
+
+
+def format_exemplars(hits: list[Hit]) -> str:
+    lines = []
+    for h in hits:
+        m = h.metadata
+        stmt = (h.content_md or h.text).split("## Solución")[0].strip().replace("\n", " ")[:500]
+        idea = (m.get("context_summary") or "")[:400].replace("\n", " ")
+        figs = "; ".join((f.get("description") or "")[:200] for f in h.figures) if h.figures else ""
+        lines.append(f"[{h.citation.citation_id}] {stmt} — {idea} — {h.citation.label}" + (f" — figure: {figs}" if figs else ""))
+    return "\n".join(lines) or "(none)"
+
+
+class InvalidLLMOutput(Exception):
+    """El modelo no devolvió JSON válido ni en el reintento (p.ej. generación degenerada hasta
+    `max_tokens`): el problema cuenta como fallo del sistema, no como error de infraestructura."""
+
+    def __init__(self, agent: str, tokens_in: int, tokens_out: int, calls: int, model: str):
+        super().__init__(f"{agent}: salida JSON inválida tras {calls} llamadas")
+        self.agent, self.tokens_in, self.tokens_out, self.calls, self.model = agent, tokens_in, tokens_out, calls, model
+
+
+class Agents:
+    def __init__(self, llm: LLM, config: dict | None = None, trace_dir: str = "data/eval/traces", versions: dict | None = None):
+        self.llm = llm
+        self.cfg = config or load_agents_config()
+        self.trace_dir = trace_dir
+        self.versions = versions or yaml.safe_load(open("configs/versions.yaml", encoding="utf-8"))
+
+    def _versions_pin(self) -> VersionsPin:
+        return VersionsPin(
+            embedding_model=self.versions["embedding"]["model"],
+            reranker_model=self.versions["reranker"]["model"],
+            index_version=self.versions["index"]["version"],
+            mathlib_tag=self.versions["lean"]["mathlib_tag"],
+            mathlib_table=mathlib_table_name(),
+        )
+
+    def _call(self, agent: str, prompt: str, schema_model, run_id: str, problem_id: str, attempt: int, images=()):
+        t0 = time.time()
+        resp = self.llm.generate(prompt, schema=schema_model.model_json_schema(), images=images, system=self.cfg["prompts"]["system"])
+        try:
+            out = schema_model.model_validate_json(resp.text)
+        except ValueError:  # JSON truncado por `max_tokens` o inválido: un reintento con el doble de tokens (cuenta en el presupuesto)
+            resp2 = self.llm.generate(prompt, schema=schema_model.model_json_schema(), images=images, system=self.cfg["prompts"]["system"], max_tokens=2 * int(getattr(self.llm, "max_tokens", None) or 4000))
+            resp = LLMResponse(text=resp2.text, model=resp2.model, tokens_in=resp.tokens_in + resp2.tokens_in, tokens_out=resp.tokens_out + resp2.tokens_out, calls=resp.calls + resp2.calls, cost_usd=resp.cost_usd + resp2.cost_usd, attempts=resp.attempts + resp2.attempts)
+            try:
+                out = schema_model.model_validate_json(resp2.text)
+            except ValueError as e:
+                # ACC-1: el evento del intento roto lleva sus propios llm_calls/tokens/costo (antes
+                # `self.trace()` los ponía siempre en 0, aunque sí se habían gastado).
+                append_event(
+                    TraceEvent(
+                        run_id=run_id,
+                        problem_id=problem_id,
+                        attempt=attempt,
+                        agent=agent,
+                        latency_ms=(time.time() - t0) * 1000,
+                        llm_calls=resp.calls,
+                        tokens=resp.tokens_in + resp.tokens_out,
+                        request={"model": resp.model, "tokens_in": resp.tokens_in, "tokens_out": resp.tokens_out, "cost_usd": round(resp.cost_usd, 6), "attempts": resp.attempts, "decision": {"invalid_json": str(e)[:200]}},
+                        versions=self._versions_pin(),
+                    ),
+                    base_dir=self.trace_dir,
+                )
+                raise InvalidLLMOutput(agent, resp.tokens_in, resp.tokens_out, resp.calls, resp.model) from e
+        # RF-7: decisión tomada por el agente (salida validada, truncada) junto a tokens y latencia
+        decision = {k: (v[:600] if isinstance(v, str) else v) for k, v in out.model_dump().items()}
+        append_event(
+            TraceEvent(
+                run_id=run_id,
+                problem_id=problem_id,
+                attempt=attempt,
+                agent=agent,
+                latency_ms=(time.time() - t0) * 1000,
+                llm_calls=1,
+                tokens=resp.tokens_in + resp.tokens_out,
+                request={"model": resp.model, "prompt_chars": len(prompt), "prompt_version": str(self.cfg["prompt_version"]), "tokens_in": resp.tokens_in, "tokens_out": resp.tokens_out, "cost_usd": round(resp.cost_usd, 6), "attempts": resp.attempts, "decision": decision},
+                versions=self._versions_pin(),
+            ),
+            base_dir=self.trace_dir,
+        )
+        return out, resp
+
+    def trace(self, agent: str, run_id: str, problem_id: str, attempt: int, latency_ms: float, decision: dict) -> None:
+        """Evento de traza para pasos sin LLM (verificador): veredicto + latencia (RF-5, RF-7)."""
+        append_event(TraceEvent(run_id=run_id, problem_id=problem_id, attempt=attempt, agent=agent, latency_ms=latency_ms, llm_calls=0, tokens=0, request={"decision": decision}), base_dir=self.trace_dir)
+
+    def plan(self, problem: Problem, exemplars: list[Hit], run_id: str, attempt: int, feedback: str = "") -> tuple[PlannerOutput, object]:
+        prompt = self.cfg["prompts"]["planner"].format(informal=problem.informal_statement, formal=problem.formal_statement, exemplars=format_exemplars(exemplars), feedback=feedback or "(none)")
+        return self._call("planner", prompt, PlannerOutput, run_id, problem.problem_id, attempt)
+
+    def generate(self, problem: Problem, plan: PlannerOutput, lemmas: list[Hit], exemplars: list[Hit], feedback: str, run_id: str, attempt: int) -> tuple[GeneratorOutput, object]:
+        plan_txt = f"Strategy: {plan.strategy}\n" + "\n".join(f"{s.subgoal_id}. {s.statement_nl} (hint: {s.formal_hint})" for s in plan.subgoals)
+        images = [f["image_path"] for h in exemplars[:2] for f in h.figures[:1] if f.get("image_path")] if self.cfg.get("llm_supports_vision") else []
+        prompt = self.cfg["prompts"]["generator"].format(informal=problem.informal_statement, formal=problem.formal_statement, plan=plan_txt, lemmas=format_lemmas(lemmas), exemplars=format_exemplars(exemplars), feedback=feedback or "(none)")
+        n = int(self.cfg.get("generator_samples", 1) or 1)
+        if n <= 1:
+            return self._call("generator", prompt, GeneratorOutput, run_id, problem.problem_id, attempt, images=images)
+        samples = [self._call("generator", prompt, GeneratorOutput, run_id, problem.problem_id, attempt, images=images) for _ in range(n)]
+        best = max(range(n), key=lambda i: sum(_jaccard(samples[i][0].sketch, samples[j][0].sketch) for j in range(n) if j != i))
+        out, resp = samples[best]
+        # BUG-5: cost_usd y attempts de las n muestras también se suman (antes se perdían: costaba
+        # como si cada muestra hubiese costado 0 y 1 intento, aunque alguna hubiese reintentado).
+        resp = type(resp)(resp.text, resp.model, sum(r.tokens_in for _, r in samples), sum(r.tokens_out for _, r in samples), calls=n, cost_usd=sum(r.cost_usd for _, r in samples), attempts=sum(r.attempts for _, r in samples))
+        return out, resp
+
+    def formalize(self, problem: Problem, sketch: str, lemmas: list[Hit], lean_error: str, run_id: str, attempt: int, skeleton: bool = False, proved: list[str] = ()) -> tuple[FormalizerOutput, object]:
+        if skeleton:  # docs/PLAN_MEJORA_RAG.md Fase 2: `have … := by sorry` por afirmación; los goals se cierran después
+            prompt = self.cfg["prompts"]["formalizer_skeleton"].format(formal=problem.formal_statement, sketch=sketch, lemmas=format_lemmas(lemmas), proved="\n".join(proved) or "(none)", lean_error=lean_error or "(none)")
+        else:
+            prompt = self.cfg["prompts"]["formalizer"].format(formal=problem.formal_statement, sketch=sketch, lemmas=format_lemmas(lemmas), lean_error=lean_error or "(none)")
+        out, resp = self._call("formalizer", prompt, FormalizerOutput, run_id, problem.problem_id, attempt)
+        out.proof_tactics = strip_code_fences(out.proof_tactics)
+        return out, resp
+
+    def sketch(self, problem: Problem, feedback: str, run_id: str, attempt: int) -> tuple[str, LLMResponse]:
+        """Esqueleto de la prueba en Lean (pasos `have … := by sorry`), en TEXTO: con salida JSON y razonamiento el
+        modelo gastaba todo su presupuesto y devolvía vacío (DECISIONS #124). La extracción la hace el grafo."""
+        t0 = time.time()
+        prompt = self.cfg["prompts"]["sketcher"].format(informal=problem.informal_statement, formal=f"{problem.header}\n\n{problem.formal_statement}".strip(), feedback=feedback or "(none)")
+        resp = self.llm.generate(prompt, system=self.cfg["prompts"]["system"], max_tokens=self.cfg.get("sketch_max_tokens"))
+        append_event(TraceEvent(run_id=run_id, problem_id=problem.problem_id, attempt=attempt, agent="sketcher", latency_ms=(time.time() - t0) * 1000, llm_calls=resp.calls, tokens=resp.tokens_in + resp.tokens_out, request={"model": resp.model, "prompt_chars": len(prompt), "prompt_version": str(self.cfg["prompt_version"]), "tokens_in": resp.tokens_in, "tokens_out": resp.tokens_out, "cost_usd": round(resp.cost_usd, 6), "attempts": resp.attempts, "decision": {"sketch": resp.text[-2000:]}}, versions=self._versions_pin()), base_dir=self.trace_dir)
+        return resp.text, resp
+
+    def fill(self, problem: Problem, goals_txt: str, run_id: str, attempt: int) -> tuple[FillOutput, object]:
+        prompt = self.cfg["prompts"]["fill"].format(formal=problem.formal_statement, goals=goals_txt)
+        out, resp = self._call("fill", prompt, FillOutput, run_id, problem.problem_id, attempt)
+        for p in out.proofs:
+            p.tactics = strip_code_fences(p.tactics)
+        return out, resp
+
+    def critique(self, problem: Problem, sketch: str, lean_code: str, lean_error: str, history: list[dict], run_id: str, attempt: int) -> tuple[CriticOutput, object]:
+        hist = "\n".join(f"attempt {h['attempt']}: {h.get('error_type', '?')} — {h.get('summary', '')[:200]}" for h in history) or "(first attempt)"
+        prompt = self.cfg["prompts"]["critic"].format(formal=problem.formal_statement, sketch=sketch, lean_code=lean_code, lean_error=lean_error, history=hist)
+        return self._call("critic", prompt, CriticOutput, run_id, problem.problem_id, attempt)
+
+    def baseline(self, mode: str, problem: Problem, run_id: str) -> tuple[BaselineAOutput | BaselineBOutput, object]:
+        prompt = self.cfg["prompts"][mode].format(formal=problem.formal_statement, informal=problem.informal_statement)
+        out, resp = self._call(mode, prompt, BaselineAOutput if mode == "baseline_a" else BaselineBOutput, run_id, problem.problem_id, 1)
+        if mode == "baseline_a":
+            out.proof_tactics = strip_code_fences(out.proof_tactics)
+        return out, resp
+
+
+def _jaccard(a: str, b: str) -> float:
+    ta, tb = set(re.findall(r"[\w^+\-*/=<>≤≥]+", a.lower())), set(re.findall(r"[\w^+\-*/=<>≤≥]+", b.lower()))
+    return len(ta & tb) / len(ta | tb) if ta | tb else 0.0
+
+
+def strip_code_fences(code: str) -> str:
+    """Quita vallas ```lean, un enunciado repetido, y la sangría común (el LLM suele traer las
+    tácticas ya indentadas a 2 espacios; `splice_proof` las vuelve a indentar, y si sólo la
+    primera línea perdía la sangría el bloque quedaba mal anidado y Lean daba `unsolved goals`)."""
+    code = re.sub(r"^\s*```[a-zA-Z0-9]*\n?", "", code.rstrip())
+    code = re.sub(r"\n?```$", "", code)
+    # si el modelo repitió el enunciado, quedarse con lo que sigue a `:= by`
+    m = re.search(r":=\s*by\s*\n", code)
+    if code.lstrip().startswith(("theorem", "lemma", "example")) and m:
+        code = code[m.end():]
+    code = re.sub(r"^\s*(?::=\s*)?by[ \t]*\n", "", code)  # el modelo a veces empieza con un `by` suelto (8/30 intentos en eval_v1): sobra, el empalme ya lo pone
+    code = textwrap.dedent(code.strip("\n")).strip("\n")
+    # la primera línea llega sin sangría y las demás con la del editor del modelo ("rcases h1 …\n  rcases h2 …",
+    # smoke 2026-10-14: Lean daba `unexpected identifier`): si la primera línea no abre un bloque, el resto
+    # baja a su nivel
+    lines = code.splitlines()
+    rest = [l for l in lines[1:] if l.strip()]
+    if rest and not lines[0].startswith("calc") and not re.search(r"(\bby|:=|=>|\bwith|\bdo|\bthen|\belse|\bfrom|[,(⟨\[])\s*$", lines[0]):
+        k = min(len(l) - len(l.lstrip()) for l in rest)
+        if k:
+            code = "\n".join([lines[0]] + [l[k:] if l.strip() else l for l in lines[1:]])
+    return code

ragsolver/agents/schemas.py

@@ -0,0 +1,122 @@
+"""Contratos JSON Schema de los agentes (RNF-4; docs/PLAN_RAG.md §8.3, propuesta §6.3).
+
+Cada agente es una función pura `state -> delta` cuya salida LLM se valida contra
+uno de estos modelos (`model_json_schema()` va como `response_format` al LLM).
+"""
+
+from __future__ import annotations
+
+from typing import Literal
+
+from pydantic import BaseModel, Field
+
+from ragsolver.rag.schema import Citation
+
+ErrorType = Literal["lean_syntax", "missing_lemma", "misformalization", "timeout", "planning", "unknown"]
+CriticAction = Literal["retry", "replan", "abandon"]
+
+
+class Problem(BaseModel):
+    problem_id: str
+    source: str = "trivial"  # trivial | minif2f_v2 | putnambench
+    split: str = "dev"
+    informal_statement: str
+    formal_statement: str  # `theorem foo ... := by sorry`
+    area: str = ""
+    difficulty: int | None = None
+    imports: list[str] = Field(default_factory=list)  # imports adicionales al de configs/agents.yaml
+    header: str = ""  # p.ej. `open BigOperators Real Nat Topology` (miniF2F); sin imports
+
+
+class Subgoal(BaseModel):
+    subgoal_id: str
+    statement_nl: str
+    formal_hint: str = ""
+    search_queries: list[str] = Field(default_factory=list, max_length=3)
+    math_area: str = ""
+
+
+class PlannerOutput(BaseModel):
+    strategy: str
+    subgoals: list[Subgoal] = Field(min_length=1, max_length=6)
+
+
+class GeneratorOutput(BaseModel):
+    sketch: str
+    used_citations: list[str] = Field(default_factory=list)  # ids M*/I*
+
+
+class FormalizerOutput(BaseModel):
+    proof_tactics: str  # sólo el cuerpo tras `:= by` — el enunciado no lo toca el LLM
+    notes: str = ""
+
+
+class GoalProof(BaseModel):
+    goal_id: str  # "G1", "G2", … en el orden en que se le mostraron los goals
+    tactics: str  # bloque que reemplaza el `sorry` de ese goal
+
+
+class FillOutput(BaseModel):
+    """FILL (docs/PLAN_MEJORA_RAG.md §4.1): pruebas de los goals que la batería CLOSE no cerró."""
+
+    proofs: list[GoalProof] = Field(default_factory=list)
+
+
+class CriticOutput(BaseModel):
+    error_type: ErrorType
+    action: CriticAction
+    missing_identifiers: list[str] = Field(default_factory=list)
+    feedback: str
+
+
+class BaselineAOutput(BaseModel):
+    """Línea base A: un solo LLM escribe la prueba Lean. Sólo el campo que la línea base produce, y
+    obligatorio: con un esquema común de campos opcionales DeepSeek dejaba `proof_tactics` vacío y
+    escribía la prueba en lenguaje natural (58/60 pruebas vacías, DECISIONS #65)."""
+
+    proof_tactics: str  # como FormalizerOutput: sólo el cuerpo tras `:= by`
+    notes: str = ""
+
+
+class BaselineBOutput(BaseModel):
+    """Línea base B: prueba en lenguaje natural + autoevaluación (sin verificación)."""
+
+    natural_language_proof: str
+    self_assessed_correct: bool
+
+
+class Verdict(BaseModel):
+    ok: bool
+    errors: list[dict] = Field(default_factory=list)  # {line, col, message}
+    uses_sorry: bool = False
+    axioms: list[str] = Field(default_factory=list)  # VER-1: `#print axioms`; ok=True exige subconjunto de STANDARD_AXIOMS
+    used_constants: list[str] = Field(default_factory=list)  # constantes del término aceptado (REPL `all_tactics`): `used_in_proof` real
+    seconds: float = 0.0
+    lean_file: str = ""
+    raw: str = ""
+
+
+class SolutionReport(BaseModel):
+    problem_id: str
+    config: str
+    status: Literal["done", "fail", "error"]
+    attempts: int = 0
+    replans: int = 0
+    llm_calls: int = 0
+    retrieval_calls: int = 0  # búsquedas del retriever (0 llamadas LLM cada una)
+    tokens_in: int = 0
+    tokens_out: int = 0
+    wall_seconds: float = 0.0
+    lean_code: str = ""
+    verdict: Verdict | None = None
+    citations: list[Citation] = Field(default_factory=list)  # con used_in_proof / used_in_sketch resueltos
+    n_retrieved: int = 0
+    n_used_in_sketch: int = 0
+    n_used_in_proof: int = 0
+    error_types: list[str] = Field(default_factory=list)  # taxonomía por intento
+    re_retrievals: int = 0
+    re_retrievals_ok: int = 0
+    models: list[str] = Field(default_factory=list)
+    self_assessed_correct: bool | None = None  # sólo línea base B
+    solved_by: str = ""  # prover_root | prover_goal | agents | auto (docs/PLAN_REDISENO_PROVER.md)
+    prover_samples: int = 0  # muestras del demostrador local (0 API)

ragsolver/cli.py

@@ -0,0 +1,33 @@
+"""CLI `ragsolver` (docs/PLAN_RAG.md Fase 2 tarea 9, Fase 3 tarea 7).
+
+  ragsolver search "..." [--corpus mathlib|informal] [--mode nl|formal|error|exemplar] [--k 8]
+  ragsolver ingest --pdf <pdf> [--skip-llm] [--sections none|front|all]
+"""
+
+from __future__ import annotations
+
+import sys
+
+
+def main(argv: list[str] | None = None) -> None:
+    argv = sys.argv[1:] if argv is None else argv
+    cmd, rest = (argv[0], argv[1:]) if argv else ("", [])
+    if cmd == "search":
+        from ragsolver.rag.retrieve import _cli
+
+        _cli(rest)
+    elif cmd == "ingest":
+        import json
+
+        from ragsolver.rag.ingest_informal import run
+
+        args = dict(zip(rest[::2], rest[1::2]))
+        rep = run(args.get("--pdf", "problemas resueltos olimpiadas.pdf"), args.get("--mineru-dir"), skip_llm="--skip-llm" in rest, sections=args.get("--sections", "none"))
+        print(json.dumps({k: v for k, v in rep.items() if k not in ("gaps", "formula_diffs")}, indent=2, ensure_ascii=False))
+    else:
+        print(__doc__)
+        sys.exit(0 if cmd in ("", "-h", "--help") else 2)
+
+
+if __name__ == "__main__":
+    main()

ragsolver/lean/verify.py

@@ -0,0 +1,491 @@
+"""Verificador (Rol B): el kernel de Lean 4 es la única fuente de verdad.
+
+Modelo de amenazas (docs/AUDIT_2026-09-23.md SEC-1/VER-1; niveles de
+https://lean-lang.org/doc/reference/latest/ValidatingProofs/). El texto de
+tácticas lo escribe un LLM que puede venir de un proveedor no confiable
+(DECISIONS #62 enruta a varios) o estar contaminado por un corpus de terceros
+(prompt injection). Antes de mandarlo a Lean:
+  1. `find_forbidden_tactic` (nivel 1: nada de comandos/metaprogramación)
+     rechaza `#comando`, metaprogramación, declaraciones nuevas, cambios de
+     entorno y caminos que no pasan por el kernel (`sorry`, `native_decide`,
+     `decide +native`). El Autoformalizador sólo puede devolver tácticas.
+  2. Tras un veredicto sin errores, se audita `#print axioms <nombre>`
+     (nivel 2): sólo se acepta si usa como mucho `propext`, `Classical.choice`
+     y `Quot.sound` — si aparece `Lean.trustCompiler`/`Lean.ofReduceBool` hubo
+     evaluación nativa, no verificación del kernel (Kimina-Prover tuvo 15/225
+     soluciones así: github.com/MoonshotAI/Kimina-Prover-Preview/issues/11).
+No hay sandbox de sistema operativo todavía (Fase 10 de docs/PLAN_CORRECCIONES.md):
+esto no protege contra bugs del elaborador de Lean en sí, ni limita el uso de
+CPU/disco de una táctica válida pero cara (el heartbeat sólo limita pasos de
+elaboración).
+
+Dos backends con el mismo `Verdict`:
+- `LeanChecker` (por defecto): REPL persistente vía `lean-interact` — `import Mathlib`
+  una sola vez (~3-5 min) y después ~0.3 s por teorema (medido, docs/DECISIONS.md #40).
+- `verify(...)`: un proceso `lake env lean` por verificación (sin estado; ~3 min
+  cada uno por el import). Respaldo y prueba de humo.
+
+El enunciado NUNCA lo escribe el LLM: se toma del problema y sólo se sustituye
+`sorry` por las tácticas — así el LLM no puede debilitar el teorema.
+"""
+
+from __future__ import annotations
+
+import os
+import re
+import textwrap
+import threading
+import subprocess
+import time
+from pathlib import Path
+
+from ragsolver.agents.schemas import Verdict
+
+_MSG_RE = re.compile(r"^(?P<file>[^\n:]+\.lean):(?P<line>\d+):(?P<col>\d+): (?P<sev>error|warning|info): ?(?P<msg>.*)$")
+
+# ---------------------------------------------------------------------------
+# Validación de tácticas (SEC-1). El Autoformalizador sólo debe devolver el
+# bloque tras `:= by` (docs/PLAN_RAG.md §6, Fase 4 tarea 4); cualquier otra
+# cosa es sospechosa.
+# ---------------------------------------------------------------------------
+
+_COMMENT_RE = re.compile(r"--[^\n]*|/-.*?-/", re.S)
+# `open Foo in <táctica>` sólo trae un nombre a escala: no ejecuta código, se permite.
+_SAFE_OPEN_IN_RE = re.compile(r"\bopen(?:\s+[A-Za-z_][\w'.]*)+\s+in\b")
+# `#eval`/`#print`/... en CUALQUIER posición, no sólo al inicio de línea: `open X in
+# #eval ...` es sintaxis válida de Lean y sería un bypass de un chequeo anclado a línea.
+_HASH_CMD_RE = re.compile(r"#[A-Za-z_]")
+_SORRY_RE = re.compile(r"(?<![\w'])sorry(?![\w'])")
+_NATIVE_DECIDE_RE = re.compile(r"\bdecide\s*\+\s*native\b")
+_IO_RE = re.compile(r"\bIO\.")
+_DENIED_WORD_RE = re.compile(
+    r"(?<![\w'])("
+    r"sorry|admit|native_decide|axiom|opaque"
+    r"|ofReduceBool|trustCompiler"  # el axioma detrás de native_decide/decide +native (VER-1); rechazo temprano por nombre, además de la auditoría de axiomas
+    r"|run_tac|run_cmd|run_elab|elab_rules|elab|macro_rules|macro|notation|infix|infixl|infixr|prefix|postfix"
+    r"|attribute|unsafe|implemented_by|extern"
+    r"|set_option|import|open"
+    r"|theorem|lemma|def|abbrev|instance|example|structure|inductive|class|namespace|section|end"
+    r")(?![\w'])"
+)
+
+
+def find_forbidden_tactic(proof_tactics: str) -> str | None:
+    """Primer patrón prohibido en el texto de tácticas, o None si es seguro: sin
+    `#comando`, sin metaprogramación, sin declaraciones nuevas, sin cambios de
+    entorno (salvo `open X in`) y sin caminos que evitan el kernel (`sorry`,
+    `native_decide`, `decide +native`, `IO.*`)."""
+    stripped = _COMMENT_RE.sub(" ", proof_tactics)
+    if _HASH_CMD_RE.search(stripped):
+        return "#-command"
+    if _NATIVE_DECIDE_RE.search(stripped):
+        return "decide +native"
+    if _IO_RE.search(stripped):
+        return "IO."
+    stripped = _SAFE_OPEN_IN_RE.sub(" ", stripped)
+    m = _DENIED_WORD_RE.search(stripped)
+    return m.group(1) if m else None
+
+
+# ---------------------------------------------------------------------------
+# Auditoría de axiomas (VER-1). "Si aparece Lean.trustCompiler, la evaluación
+# nativa se usó" en vez del kernel (guía oficial de Lean, enlace arriba).
+# ---------------------------------------------------------------------------
+
+_AXIOMS_RE = re.compile(r"depends on axioms:\s*\[([^\]]*)\]")
+STANDARD_AXIOMS = frozenset({"propext", "Classical.choice", "Quot.sound"})
+
+
+def parse_axioms(text: str) -> list[str]:
+    """Extrae la lista de `#print axioms <name>` ("depends on axioms: [...]";
+    sin coincidencia -> "no depende de ningún axioma" -> lista vacía)."""
+    m = _AXIOMS_RE.search(text)
+    return [a.strip() for a in m.group(1).split(",") if a.strip()] if m else []
+
+
+def non_standard_axioms(axioms: list[str]) -> list[str]:
+    return [a for a in axioms if a not in STANDARD_AXIOMS]
+
+
+def _axiom_check(errors: list[dict], uses_sorry: bool, axioms: list[str]) -> tuple[bool, list[dict]]:
+    """ok sólo si no hay errores, no usa `sorry` y los axiomas son un subconjunto
+    de los estándar; si no, agrega un error legible (para el Crítico) sin perder
+    los que ya había."""
+    if errors or uses_sorry:
+        return False, errors
+    bad = non_standard_axioms(axioms)
+    if bad:
+        return False, errors + [{"line": 0, "col": 0, "message": f"non-standard axioms: {', '.join(bad)}"}]
+    return True, errors
+
+
+# ---------------------------------------------------------------------------
+# Fuente única REPL <-> reporte (BUG-2): una sola función construye el bloque
+# que se verifica Y el que se reporta, para que no puedan divergir.
+# ---------------------------------------------------------------------------
+
+_THEOREM_NAME_RE = re.compile(r"^\s*(?:theorem|lemma)\s+([A-Za-z_][\w'.]*)")
+
+
+def _lean_project() -> Path:
+    """`RAGSOLVER_LEAN_PROJECT` > copia en ext4 (~/ragsolver_cache/lean_project, misma tag,
+    10x más rápida que /mnt/c para cargar los .olean de Mathlib) > lean_project/ del repo."""
+    env = os.environ.get("RAGSOLVER_LEAN_PROJECT")
+    if env:
+        return Path(env)
+    cache = Path.home() / "ragsolver_cache" / "lean_project"
+    if (cache / ".lake" / "packages" / "mathlib" / ".lake" / "build").exists():
+        return cache
+    return Path(__file__).resolve().parents[3] / "lean_project"
+
+
+LEAN_PROJECT = _lean_project()
+
+
+def splice_proof(formal_statement: str, proof_tactics: str) -> str:
+    """Reemplaza el `sorry` final del enunciado por el bloque de tácticas (indentado)."""
+    stmt = formal_statement.rstrip()
+    tactics = textwrap.dedent(proof_tactics.strip("\n"))  # sangría común fuera; la relativa (bloques `have ... := by`) se conserva
+    body = "\n".join("  " + line if line.strip() else "" for line in tactics.splitlines())
+    for pat in (r":=\s*by\s+sorry\s*$", r":=\s*sorry\s*$"):
+        if re.search(pat, stmt):
+            return re.sub(pat, lambda _m: ":= by\n" + body, stmt)
+    return stmt + " := by\n" + body
+
+
+_HAVE_BY_RE = re.compile(r"^have\b.*:=\s*by\b(.*)$")
+
+
+def skeletonize(proof: str) -> tuple[str, list[str | None]]:
+    """Prueba del LLM -> (esqueleto, candidatos), docs/PLAN_MEJORA_RAG.md Fase 2.
+
+    El modelo casi nunca escribe el esqueleto con `sorry` que se le pide: escribe la prueba entera
+    (smoke del 2026-10-14). En vez de depender de que obedezca, cada `have … := by <bloque>` de nivel
+    superior pasa a `have … := by sorry` y su bloque queda como **candidato** para ese goal; las líneas
+    tras el último `have` (el cierre) pasan a un `sorry` con ese cierre como candidato. Sin `have`, la
+    prueba entera es el candidato del goal raíz. El resto (`rcases`, `intro`, `have … := término`) queda
+    tal cual. `candidatos[k]` corresponde al k-ésimo `sorry` del esqueleto (None = no hay candidato).
+    """
+    lines = textwrap.dedent(proof.strip("\n")).splitlines()
+    top = lambda l: bool(l.strip()) and not l[0].isspace()
+    blocks = []  # (inicio, fin exclusivo, cabecera, candidato)
+    i = 0
+    while i < len(lines):
+        m = _HAVE_BY_RE.match(lines[i]) if top(lines[i]) else None
+        if not m:
+            i += 1
+            continue
+        j = i + 1
+        while j < len(lines) and not top(lines[j]):
+            j += 1
+        inline = m.group(1).strip()
+        body = textwrap.dedent("\n".join(lines[i + 1 : j])).strip("\n")
+        block = "\n".join(x for x in (inline, body) if x)
+        blocks.append((i, j, lines[i][: m.start(1)].rstrip(), block))
+        i = j
+    if not blocks:
+        body = "\n".join(lines).strip("\n")
+        return "sorry", [None if not body or body == "sorry" else body]
+    out: list[str] = []
+    cands: list[str | None] = []
+    pos = 0
+    for start, end, head, block in blocks:
+        for l in lines[pos:start]:
+            out.append(l)
+            cands += [None] * count_sorries(l)
+        out.append(f"{head} sorry")
+        cands.append(None if not block or block == "sorry" else block)
+        pos = end
+    tail = "\n".join(lines[pos:]).strip("\n")
+    if tail:
+        out.append("sorry")
+        cands.append(None if tail == "sorry" else tail)
+    return "\n".join(out), cands
+
+
+def count_sorries(skeleton: str) -> int:
+    return len(_SORRY_RE.findall(skeleton))
+
+
+def fill_sorries(skeleton: str, blocks: list[str]) -> str:
+    """Reemplaza el k-ésimo `sorry` del esqueleto por `blocks[k]` (docs/PLAN_MEJORA_RAG.md Fase 2).
+    Un bloque de una línea va en el lugar del `sorry`; uno de varias líneas va en líneas nuevas con
+    la sangría de la línea del `sorry` + 2, salvo que al `sorry` le siga texto en la misma línea
+    (`exact foo (by sorry)`): entonces va entre paréntesis y separado por `;`."""
+    it = iter(blocks)
+    out = []
+    for line in skeleton.splitlines():
+        parts = _SORRY_RE.split(line)
+        if len(parts) == 1:
+            out.append(line)
+            continue
+        pad = " " * (len(line) - len(line.lstrip()) + 2)
+        new = parts[0]
+        for rest in parts[1:]:
+            block = textwrap.dedent(next(it, "sorry").strip("\n")).strip("\n")
+            if "\n" not in block:
+                new += block
+            elif rest.strip():
+                new += "(" + "; ".join(l.strip() for l in block.splitlines() if l.strip()) + ")"
+            else:
+                new = new.rstrip() + "\n" + "\n".join(pad + l if l.strip() else "" for l in block.splitlines())
+            new += rest
+        out.append(new)
+    return "\n".join(out)
+
+
+def theorem_block(formal_statement: str, proof_tactics: str, header: str = "", max_heartbeats: int = 400000) -> tuple[str, str]:
+    """Bloque que se envía al REPL (sin `import`: ya está en el entorno) y que
+    también se reporta como `lean_code` vía `build_file` (BUG-2): `open`s del
+    header + `set_option maxHeartbeats N in` + el enunciado con las tácticas
+    empalmadas + `#print axioms <nombre>` para la auditoría de VER-1. Devuelve
+    (código, nombre del teorema).
+
+    `formal_statement` debe empezar con `theorem <nombre>` o `lemma <nombre>`
+    (el formato que exige `Problem.formal_statement`); un `example` anónimo se
+    renombra de forma determinista y mecánica (no lo hace el LLM) para poder
+    auditar sus axiomas."""
+    stmt = formal_statement.rstrip()
+    m = _THEOREM_NAME_RE.match(stmt)
+    if m:
+        name = m.group(1)
+    elif stmt.lstrip().startswith("example"):
+        name = "_ragsolver_goal"
+        stmt = re.sub(r"^\s*example\b", f"theorem {name}", stmt, count=1)
+    else:
+        raise ValueError(f"formal_statement debe empezar con 'theorem', 'lemma' o 'example': {stmt[:60]!r}")
+    opens = "\n".join(l for l in header.splitlines() if l.strip() and not l.strip().startswith("import"))
+    code = (opens + "\n" if opens else "") + f"set_option maxHeartbeats {max_heartbeats} in\n" + splice_proof(stmt, proof_tactics) + f"\n#print axioms {name}"
+    return code, name
+
+
+def build_file(formal_statement: str, proof_tactics: str, imports: list[str], max_heartbeats: int = 400000, header: str = "") -> str:
+    """Archivo Lean completo y autocontenido: el mismo texto que se le pide al
+    REPL, más el `import` inicial (que ahí ya viene del entorno). Es el
+    `lean_code` que se reporta (BUG-2): reproduce exactamente lo verificado,
+    incluidos los `open` del header."""
+    block, _ = theorem_block(formal_statement, proof_tactics, header, max_heartbeats)
+    hdr = "\n".join(f"import {m}" for m in dict.fromkeys(imports)) + "\n\n"
+    return hdr + block + "\n"
+
+
+def parse_messages(output: str) -> list[dict]:
+    msgs: list[dict] = []
+    for line in output.splitlines():
+        m = _MSG_RE.match(line)
+        if m:
+            msgs.append({"line": int(m["line"]), "col": int(m["col"]), "severity": m["sev"], "message": m["msg"]})
+        elif msgs:
+            msgs[-1]["message"] += "\n" + line
+    return msgs
+
+
+def run_lean(source: str, name: str, project: Path = LEAN_PROJECT, timeout_s: int = 900) -> tuple[int | None, str, float, Path]:
+    scratch = project / "scratch"
+    scratch.mkdir(exist_ok=True)
+    path = scratch / f"{re.sub(r'[^A-Za-z0-9_]+', '_', name)}.lean"
+    path.write_text(source, encoding="utf-8")
+    env = {**os.environ, "PATH": f"{Path.home() / '.elan' / 'bin'}:{os.environ.get('PATH', '')}"}
+    t0 = time.time()
+    try:
+        proc = subprocess.run(["lake", "env", "lean", str(path.relative_to(project))], cwd=project, env=env, capture_output=True, text=True, timeout=timeout_s)
+        return proc.returncode, proc.stdout + proc.stderr, time.time() - t0, path
+    except subprocess.TimeoutExpired as e:
+        return None, (e.stdout or "") + (e.stderr or "") if isinstance(e.stdout, str) else "", time.time() - t0, path
+
+
+def verify(formal_statement: str, proof_tactics: str, name: str, imports: list[str], timeout_s: int = 900, max_heartbeats: int = 400000, project: Path = LEAN_PROJECT, header: str = "") -> Verdict:
+    forbidden = find_forbidden_tactic(proof_tactics)
+    if forbidden:
+        return Verdict(ok=False, errors=[{"line": 0, "col": 0, "message": f"forbidden token in proof: {forbidden}"}])
+    source = build_file(formal_statement, proof_tactics, imports, max_heartbeats, header)
+    code, out, secs, path = run_lean(source, name, project, timeout_s)
+    msgs = parse_messages(out)
+    errors = [m for m in msgs if m["severity"] == "error"]
+    uses_sorry = any("sorry" in m["message"] for m in msgs)
+    if code is None:
+        errors.append({"line": 0, "col": 0, "message": f"timeout after {timeout_s}s"})
+        return Verdict(ok=False, errors=errors, uses_sorry=uses_sorry, seconds=round(secs, 1), lean_file=str(path), raw=out[-4000:])
+    axioms = parse_axioms("\n".join(m["message"] for m in msgs if m["severity"] == "info"))
+    ok, errors = _axiom_check(errors, uses_sorry, axioms)
+    return Verdict(ok=ok, errors=errors, uses_sorry=uses_sorry, axioms=axioms, seconds=round(secs, 1), lean_file=str(path), raw=out[-4000:])
+
+
+def limit_heartbeats(tactic: str, heartbeats: int) -> str:
+    """`set_option maxHeartbeats N in` sobre una táctica. Un bloque de varias líneas (el de un paso que escribió
+    el modelo o el demostrador) va dentro de `·`, que enfoca el goal y debe cerrarlo como el bloque en su sitio:
+    sin eso el límite no lo cubría y un bloque lento agotaba el timeout de reloj, reiniciaba el REPL y dejaba
+    "stale" los pasos de todos los hilos (eval-v4, DECISIONS #128)."""
+    body = tactic.strip()
+    if "\n" not in body:
+        return f"set_option maxHeartbeats {int(heartbeats)} in {body}"
+    return f"set_option maxHeartbeats {int(heartbeats)} in\n· " + body.replace("\n", "\n  ")
+
+
+class LeanChecker:
+    """REPL persistente: el entorno con los imports se crea una vez y se reutiliza."""
+
+    def __init__(self, imports: list[str] = ("Mathlib",), project: Path | None = None, timeout_s: int = 900):
+        self.imports = list(imports)
+        self.project = project or LEAN_PROJECT
+        self.timeout_s = timeout_s
+        self._server = None
+        self._env = None
+        self._gen = 0  # sube en cada arranque del REPL: un `proof_state` sólo vale en la generación que lo creó
+        self._lock = threading.Lock()  # un solo REPL; ~0.3 s por comprobación, no vale la pena más
+
+    @property
+    def gen(self) -> int:
+        """Generación del REPL vivo (-1 si cayó): un `proof_state` de otra generación ya no vale."""
+        return self._gen if self._server is not None else -1
+
+    def _start(self) -> None:
+        from lean_interact import Command, LeanREPLConfig, LeanServer
+        from lean_interact.project import LocalProject
+
+        os.environ["PATH"] = f"{Path.home() / '.elan' / 'bin'}:{os.environ.get('PATH', '')}"
+        self._server = LeanServer(LeanREPLConfig(project=LocalProject(directory=str(self.project), auto_build=False)))
+        self._gen += 1
+        r = self._server.run(Command(cmd="\n".join(f"import {m}" for m in dict.fromkeys(self.imports))), timeout=max(self.timeout_s, 1800))
+        errors = [m.data for m in r.messages if m.severity == "error"]
+        if errors:
+            raise RuntimeError(f"imports fallaron en el REPL: {errors[:2]}")
+        self._env = r.env
+
+    def check(self, formal_statement: str, proof_tactics: str, header: str = "", max_heartbeats: int = 400000) -> Verdict:
+        forbidden = find_forbidden_tactic(proof_tactics)
+        if forbidden:
+            return Verdict(ok=False, errors=[{"line": 0, "col": 0, "message": f"forbidden token in proof: {forbidden}"}])
+        with self._lock:
+            return self._check_locked(formal_statement, proof_tactics, header, max_heartbeats)
+
+    def _check_locked(self, formal_statement: str, proof_tactics: str, header: str, max_heartbeats: int) -> Verdict:
+        from lean_interact import Command
+
+        if self._server is None or not self._server.is_alive():
+            self._start()
+        code, _name = theorem_block(formal_statement, proof_tactics, header, max_heartbeats)
+        t0 = time.time()
+        try:
+            # all_tactics: constantes que usa cada táctica -> qué lemas citados usa DE VERDAD la prueba
+            r = self._server.run(Command(cmd=code, env=self._env, all_tactics=True), timeout=self.timeout_s)
+        except Exception as e:  # timeout o REPL caído: se reinicia en la próxima llamada
+            self._server = None
+            return Verdict(ok=False, errors=[{"line": 0, "col": 0, "message": f"lean repl failure: {type(e).__name__}: {str(e)[:200]}"}], seconds=round(time.time() - t0, 1), raw=code[-2000:])
+        msgs = [{"line": m.start_pos.line if m.start_pos else 0, "col": m.start_pos.column if m.start_pos else 0, "severity": m.severity, "message": m.data} for m in r.messages]
+        errors = [m for m in msgs if m["severity"] == "error"]
+        uses_sorry = any("sorry" in m["message"] for m in msgs)
+        axioms = parse_axioms("\n".join(m["message"] for m in msgs if m["severity"] == "info"))
+        ok, errors = _axiom_check(errors, uses_sorry, axioms)
+        used = sorted({c for t in getattr(r, "tactics", None) or [] for c in t.used_constants})
+        return Verdict(ok=ok, errors=errors, uses_sorry=uses_sorry, axioms=axioms, used_constants=used, seconds=round(time.time() - t0, 1), raw=code[-2000:])
+
+    def _run(self, query, timeout: float | None = None):
+        """Una consulta al REPL con el lock tomado por el llamador; timeout o REPL caído -> None
+        (se reinicia en la próxima llamada, y los `proof_state` anteriores dejan de valer)."""
+        if self._server is None or not self._server.is_alive():
+            self._start()
+        try:
+            return self._server.run(query, timeout=timeout or self.timeout_s)
+        except Exception:
+            self._server = None
+            return None
+
+    def goals(self, formal_statement: str, skeleton: str, header: str = "", max_heartbeats: int = 400000) -> tuple[list[dict], list[dict]]:
+        """Modo sonda (docs/PLAN_MEJORA_RAG.md Fase 2): elabora un esqueleto con `sorry` y devuelve
+        ([{goal, proof_state}] en el orden en que aparecen los `sorry`, errores de elaboración). Nunca
+        produce un `Verdict`: el único camino a `ok` sigue siendo `check` sobre el archivo final, que
+        rechaza `sorry`. Fuera de `sorry`, el esqueleto pasa por el mismo validador que una prueba."""
+        from lean_interact import Command
+
+        forbidden = find_forbidden_tactic(_SORRY_RE.sub(" skip ", skeleton))
+        if forbidden:
+            return [], [{"line": 0, "col": 0, "message": f"forbidden token in proof: {forbidden}"}]
+        code, _name = theorem_block(formal_statement, skeleton, header, max_heartbeats)
+        with self._lock:
+            r = self._run(Command(cmd=code, env=self._env))
+        if r is None or not hasattr(r, "sorries"):
+            return [], [{"line": 0, "col": 0, "message": f"lean repl failure: {str(getattr(r, 'message', r))[:200]}"}]
+        errors = [{"line": m.start_pos.line if m.start_pos else 0, "col": m.start_pos.column if m.start_pos else 0, "message": m.data} for m in r.messages if m.severity == "error"]
+        found = sorted(r.sorries, key=lambda s: (s.start_pos.line, s.start_pos.column) if s.start_pos else (0, 0))
+        return [{"goal": s.goal, "proof_state": s.proof_state, "gen": self._gen} for s in found], errors
+
+    def step(self, proof_state: int, tactic: str, timeout: float = 120, heartbeats: int | None = None, gen: int | None = None) -> tuple[bool, str, list[str]]:
+        """Aplica `tactic` a un `proof_state` de `goals` sin re-elaborar el teorema (`ProofStep`).
+        Devuelve (cerrado, error o estado, mensajes info — p.ej. el "Try this" de `try?`). La táctica
+        pasa por `find_forbidden_tactic` antes de tocar Lean, igual que en `check`."""
+        from lean_interact import ProofStep
+
+        forbidden = find_forbidden_tactic(tactic)
+        if forbidden:
+            return False, f"forbidden token in proof: {forbidden}", []
+        if heartbeats:
+            # el límite lo pone el sistema DESPUÉS del validador (que prohíbe `set_option` al LLM): Lean
+            # corta por heartbeats antes que el timeout de reloj, que reinicia el REPL (~5 min) e invalida
+            # los `proof_state` de los demás hilos
+            tactic = limit_heartbeats(tactic, heartbeats)
+        with self._lock:
+            if gen is not None and (gen != self._gen or self._server is None):
+                # el REPL se reinició (timeout de otra táctica): ese número de estado ya no existe o, peor,
+                # es otro goal del REPL nuevo
+                return False, "stale proof state (lean repl restarted)", []
+            r = self._run(ProofStep(tactic=tactic, proof_state=proof_state), timeout=timeout)
+        if r is None or not hasattr(r, "proof_status"):  # LeanError (la táctica falló) o REPL caído
+            return False, str(getattr(r, "message", "lean repl failure"))[:2000], []
+        errs = [m.data for m in r.messages if m.severity == "error"]
+        infos = [m.data for m in r.messages if m.severity == "info"]
+        return r.proof_status == "Completed" and not errs, "\n".join(errs)[:2000] or r.proof_status, infos
+
+    def signatures(self, names: list[str], header: str = "") -> dict[str, str]:
+        """{nombre: tipo} de los `names` que resuelve `#check @nombre` en el entorno cargado, uno por
+        comando (exacto, a diferencia de `check_identifiers_exist`). `header` aporta los `open` con
+        los que esos nombres se usan en las pruebas (p.ej. `open Nat` resuelve `succ_le_iff`)."""
+        from lean_interact import Command
+
+        opens = " ".join(l.strip()[len("open"):].strip() for l in header.splitlines() if l.strip().startswith("open"))
+        prefix = f"open {opens} in\n" if opens else ""
+        out: dict[str, str] = {}
+        with self._lock:
+            for n in names:
+                # con los `open`, un nombre de la raíz puede quedar ambiguo (`sq_nonneg` vs `Nat.sq_nonneg`):
+                # la prueba lo desambigua por tipo, `#check` no -> se reintenta sin los `open`
+                for pre in dict.fromkeys((prefix, "")):
+                    r = self._run(Command(cmd=f"{pre}#check @{n}", env=self._env), timeout=60)
+                    msgs = getattr(r, "messages", None)
+                    if msgs is not None and not any(m.severity == "error" for m in msgs):
+                        info = next((m.data for m in msgs if m.severity == "info"), "")
+                        out[n] = info.split(" : ", 1)[1].strip() if " : " in info else info
+                        break
+        return out
+
+    def check_identifiers_exist(self, decl_names: list[str]) -> tuple[int, int]:
+        """(existen, total): cuántos de `decl_names` resuelve el entorno cargado,
+        vía `#check @nombre`. Consistencia índice <-> Lean (`docs/PLAN_RAG.md
+        §12`): si el índice tiene `decl_name` que no existen en esta versión de
+        Mathlib, el RAG cita lemas fantasma. No es una prueba de un LLM: no pasa
+        por `find_forbidden_tactic`. Aproximado (cuenta errores totales, no los
+        mapea 1 a 1 con cada nombre) — suficiente para un aviso, no aborta nada."""
+        from lean_interact import Command
+
+        if not decl_names:
+            return 0, 0
+        with self._lock:
+            if self._server is None or not self._server.is_alive():
+                self._start()
+            code = "\n".join(f"#check @{n}" for n in decl_names)
+            try:
+                r = self._server.run(Command(cmd=code, env=self._env), timeout=self.timeout_s)
+            except Exception:
+                return 0, len(decl_names)
+        n_errors = sum(1 for m in r.messages if m.severity == "error")
+        return max(0, len(decl_names) - n_errors), len(decl_names)
+
+    def close(self) -> None:
+        if self._server is not None:
+            self._server.kill()
+            self._server = None
+
+
+def identifiers_used(proof_tactics: str, decl_names: list[str]) -> list[str]:
+    """Nombres de Mathlib citados que aparecen en el código aceptado (used_in_proof, §6.4)."""
+    return [d for d in decl_names if re.search(r"(?<![\w.'])" + re.escape(d) + r"(?![\w'.])", proof_tactics)]

ragsolver/llm.py

@@ -0,0 +1,265 @@
+"""Cliente LLM/VLM único para agentes (Fase 4) y enriquecimiento (Fase 2).
+
+Proveedores (configs/versions.yaml, secciones `llm` / `vlm_enrichment`):
+- `gemini`: REST `generativelanguage.googleapis.com` (key en GEMINI_API_KEY).
+- `openai_compatible`: `/chat/completions` con `base_url` (OpenRouter, OpenAI,
+  Ollama, vLLM...); key en la variable que diga `api_key_env`.
+
+Un solo método: `generate(prompt, schema=None, images=(), system=None)` ->
+`LLMResponse(text, model, tokens_in, tokens_out)`. Con `schema` (JSON Schema
+estándar) la salida es JSON validado; para Gemini se traduce al subconjunto
+OpenAPI que acepta `responseSchema`.
+
+Cadena de modelos: `model` + `fallback_models`; al agotar la cuota diaria de uno
+(429 con quotaId *PerDay*) se pasa al siguiente. Reintentos (LLM-1, hasta 4,
+`_MAX_ATTEMPTS`): error de transporte o 429/5xx -> 3 s / exponencial; **nunca**
+un timeout de lectura (el proveedor puede haber generado — y cobrado — la
+respuesta antes de que el timeout cortara la conexión; reintentarlo la
+duplicaría). Sin caché aquí (la tiene el Enricher).
+"""
+
+from __future__ import annotations
+
+import base64
+import json
+import os
+import threading
+from dataclasses import dataclass
+from pathlib import Path
+
+import httpx
+import yaml
+from tenacity import Retrying, retry_if_exception
+
+_GEMINI_API = "https://generativelanguage.googleapis.com/v1beta/models/{model}:generateContent"
+# ponytail: fijo, no por instancia — si algún día hace falta variar el número de reintentos entre
+# secciones (llm/vlm_enrichment), pasar `max_attempts` al constructor y usarlo en el `Retrying` de abajo.
+_MAX_ATTEMPTS = 4
+# Un 429 es una solicitud RECHAZADA (no se cobra): con el proveedor saturado ("engine_overloaded",
+# DECISIONS #103-#104) conviene esperar más en vez de perder el par con lo ya gastado.
+_MAX_ATTEMPTS_429 = 10
+
+
+class DailyQuotaExhausted(Exception):
+    """429 con quotaId *PerDay*: el modelo no vuelve hasta mañana -> cambiar de modelo."""
+
+
+@dataclass
+class LLMResponse:
+    text: str
+    model: str
+    tokens_in: int = 0
+    tokens_out: int = 0
+    calls: int = 1  # >1 cuando una respuesta agrega varias llamadas (self-consistency)
+    cost_usd: float = 0.0  # OpenRouter `usage.cost` (exacto, por proveedor); 0 si el backend no lo informa
+    attempts: int = 1  # LLM-1: cuántos intentos hizo _generate_with (reintentos de transporte/429/5xx)
+
+    def json(self) -> dict:
+        return json.loads(self.text)
+
+
+def _is_daily_quota(response: httpx.Response) -> bool:
+    try:
+        details = response.json()["error"].get("details", [])
+    except Exception:
+        return False
+    return any("PerDay" in v.get("quotaId", "") for d in details for v in d.get("violations", []))
+
+
+def _retryable(exc: BaseException) -> bool:
+    if isinstance(exc, httpx.HTTPStatusError):
+        return exc.response.status_code in (429, 500, 502, 503, 504)
+    if isinstance(exc, httpx.ReadTimeout):
+        # LLM-1: un timeout de LECTURA puede significar que el proveedor ya generó (y cobró) la
+        # respuesta y el corte fue nuestro; reintentar la duplicaría. ConnectTimeout y el resto de
+        # TransportError sí son seguros de reintentar (nada se envió o el proveedor no respondió nada).
+        return False
+    # JSON truncado/degenerado NO se reintenta aquí: cada intento cuesta `max_tokens` de salida y
+    # el reintento con `stop_after_attempt` alto no los contaba — fue la causa del sobrecosto de
+    # eval_v1 (DECISIONS #59). El único reintento (con el doble de tokens) lo hace `Agents._call`,
+    # y se contabiliza.
+    return isinstance(exc, httpx.TransportError)
+
+
+def _wait(retry_state) -> float:
+    exc = retry_state.outcome.exception()
+    if isinstance(exc, httpx.HTTPStatusError) and exc.response.status_code == 429:
+        return min(90.0, 4.0 * 2 ** (retry_state.attempt_number - 1))
+    return 3.0
+
+
+def _stop(retry_state) -> bool:
+    exc = retry_state.outcome.exception()
+    is_429 = isinstance(exc, httpx.HTTPStatusError) and exc.response.status_code == 429
+    return retry_state.attempt_number >= (_MAX_ATTEMPTS_429 if is_429 else _MAX_ATTEMPTS)
+
+
+def _log_retry(retry_state) -> None:
+    exc = retry_state.outcome.exception()
+    print(f"[llm retry] intento {retry_state.attempt_number} falló: {type(exc).__name__}: {str(exc)[:150]}", flush=True)
+
+
+def _gemini_schema(schema: dict) -> dict:
+    """JSON Schema (Pydantic) -> subconjunto OpenAPI de Gemini: resuelve `$ref`/`$defs`,
+    tipos en mayúsculas, `anyOf [X, null]` -> X nullable, sin claves no soportadas."""
+    defs = schema.get("$defs", {}) if isinstance(schema, dict) else {}
+
+    def conv(node):
+        if isinstance(node, list):
+            return [conv(n) for n in node]
+        if not isinstance(node, dict):
+            return node
+        if "$ref" in node:
+            return conv(defs[node["$ref"].rsplit("/", 1)[1]])
+        if "anyOf" in node:
+            options = [o for o in node["anyOf"] if o.get("type") != "null"]
+            nullable = len(options) < len(node["anyOf"])
+            base = conv(options[0]) if len(options) == 1 else {"anyOf": conv(options)}
+            if nullable:
+                base["nullable"] = True
+            return base
+        out = {}
+        for k, v in node.items():
+            if k in ("additionalProperties", "$schema", "title", "default", "$defs", "definitions", "examples"):
+                continue
+            if k == "type" and isinstance(v, str):
+                out[k] = v.upper()
+            elif k == "properties":
+                out[k] = {pk: conv(pv) for pk, pv in v.items()}
+            elif k == "items":
+                out[k] = conv(v)
+            else:
+                out[k] = v
+        return out
+
+    return conv(schema)
+
+
+def _read_dotenv(name: str, path: str = ".env") -> str | None:
+    p = Path(path)
+    if not p.exists():
+        return None
+    for line in p.read_text(encoding="utf-8").splitlines():
+        if line.startswith(name + "="):
+            return line.split("=", 1)[1].strip().strip('"').strip("'")
+    return None
+
+
+class LLM:
+    def __init__(self, versions_yaml: str = "configs/versions.yaml", section: str = "llm", config: dict | None = None):
+        cfg = config or yaml.safe_load(open(versions_yaml, encoding="utf-8"))[section]
+        self.provider = cfg.get("provider", "gemini")
+        self.models: list[str] = [cfg["model"], *(cfg.get("fallback_models") or [])]
+        self.base_url = (cfg.get("base_url") or "").rstrip("/")
+        key_env = cfg.get("api_key_env") or ("GEMINI_API_KEY" if self.provider == "gemini" else "OPENROUTER_API_KEY")
+        self.api_key = os.environ.get(key_env) or _read_dotenv(key_env)
+        if not self.api_key:
+            raise RuntimeError(f"{key_env} no está en el entorno ni en .env")
+        self.temperature = float(cfg.get("temperature", 0.1))
+        self.seed = cfg.get("seed")  # RNF-2: semilla fijada en cada llamada (Gemini `seed`, OpenAI `seed`)
+        self.max_tokens = cfg.get("max_tokens")  # tope de salida (incluye el razonamiento en modelos "thinking")
+        self.reasoning_effort = cfg.get("reasoning_effort")  # OpenRouter: off | low | medium | high
+        self.timeout_s = float(cfg.get("timeout_s", 300))  # LLM-1: bajado de 600-900; 4000 tok de salida al proveedor más lento medido son ~210s (#62)
+        self.provider_routing = cfg.get("provider_routing")  # OpenRouter `provider` (max_price, sort, order…), se envía tal cual
+        self._model_idx = 0
+        self._lock = threading.Lock()
+        self.exhausted: list[str] = []
+        self.calls = 0
+        self.tokens_in = 0
+        self.tokens_out = 0
+        self.cost_usd = 0.0
+        self._client = httpx.Client(timeout=self.timeout_s)
+
+    @property
+    def model(self) -> str:
+        return self.models[self._model_idx]
+
+    def generate(self, prompt: str, schema: dict | None = None, images: tuple[str | Path, ...] | list = (), system: str | None = None, max_tokens: int | None = None) -> LLMResponse:
+        while True:
+            model = self.model
+            try:
+                return self._generate_with(model, prompt, schema, tuple(images), system, max_tokens)
+            except DailyQuotaExhausted:
+                with self._lock:
+                    if self.models[self._model_idx] == model:
+                        if self._model_idx + 1 >= len(self.models):
+                            raise
+                        self._model_idx += 1
+                        self.exhausted.append(model)
+
+    def _generate_with(self, model: str, prompt: str, schema: dict | None, images: tuple, system: str | None, max_tokens: int | None) -> LLMResponse:
+        # `Retrying` en vez del decorador `@retry`: así se cuenta el número de intentos de esta
+        # llamada (LLM-1, `resp.attempts`) sin estado compartido entre hilos (el runner usa `--workers`).
+        n_attempts = 0
+        for attempt in Retrying(retry=retry_if_exception(_retryable), wait=_wait, stop=_stop, before_sleep=_log_retry, reraise=True):
+            with attempt:
+                n_attempts += 1
+                if self.provider == "gemini":
+                    resp = self._gemini(model, prompt, schema, images, system, max_tokens)
+                else:
+                    resp = self._openai(model, prompt, schema, images, system, max_tokens)
+        resp.attempts = n_attempts
+        with self._lock:
+            self.calls += 1
+            self.tokens_in += resp.tokens_in
+            self.tokens_out += resp.tokens_out
+            self.cost_usd += resp.cost_usd
+        return resp
+
+    # -- backends ----------------------------------------------------------------
+
+    def _gemini(self, model, prompt, schema, images, system, max_tokens) -> LLMResponse:
+        parts = [{"text": prompt}] + [
+            {"inline_data": {"mime_type": "image/png", "data": base64.b64encode(Path(p).read_bytes()).decode()}} for p in images
+        ]
+        gen: dict = {"temperature": self.temperature}
+        if self.seed is not None:
+            gen["seed"] = int(self.seed)
+        if max_tokens or self.max_tokens:
+            gen["maxOutputTokens"] = int(max_tokens or self.max_tokens)
+        if schema is not None:
+            gen.update(responseMimeType="application/json", responseSchema=_gemini_schema(schema))
+        body: dict = {"contents": [{"parts": parts}], "generationConfig": gen}
+        if system:
+            body["systemInstruction"] = {"parts": [{"text": system}]}
+        r = self._client.post(_GEMINI_API.format(model=model), headers={"x-goog-api-key": self.api_key}, json=body)
+        if r.status_code == 429 and _is_daily_quota(r):
+            raise DailyQuotaExhausted(model)
+        r.raise_for_status()
+        data = r.json()
+        cand = data["candidates"][0]
+        text = "".join(p.get("text", "") for p in cand.get("content", {}).get("parts", []) if not p.get("thought"))
+        usage = data.get("usageMetadata", {})
+        return LLMResponse(text, model, usage.get("promptTokenCount", 0), usage.get("candidatesTokenCount", 0) + usage.get("thoughtsTokenCount", 0))
+
+    def _openai(self, model, prompt, schema, images, system, max_tokens) -> LLMResponse:
+        content: list[dict] = [{"type": "text", "text": prompt}] + [
+            {"type": "image_url", "image_url": {"url": "data:image/png;base64," + base64.b64encode(Path(p).read_bytes()).decode()}} for p in images
+        ]
+        messages = ([{"role": "system", "content": system}] if system else []) + [{"role": "user", "content": content}]
+        body: dict = {"model": model, "messages": messages, "temperature": self.temperature}
+        if self.seed is not None:
+            body["seed"] = int(self.seed)
+        if max_tokens or self.max_tokens:
+            body["max_tokens"] = int(max_tokens or self.max_tokens)
+        if "openrouter" in self.base_url:
+            body["usage"] = {"include": True}  # costo exacto en la respuesta
+            if self.provider_routing:
+                body["provider"] = self.provider_routing
+        if self.reasoning_effort:  # "off" = sin cadena de razonamiento (DeepSeek V4 Flash: 24 s vs 76-90 s por llamada)
+            body["reasoning"] = {"enabled": False} if self.reasoning_effort == "off" else {"effort": self.reasoning_effort}
+        if schema is not None:
+            body["response_format"] = {"type": "json_schema", "json_schema": {"name": "output", "schema": schema, "strict": False}}
+        headers = {"Authorization": f"Bearer {self.api_key}"}
+        if "openrouter" in self.base_url:
+            headers["HTTP-Referer"] = "https://github.com/ragsolver"  # atribución opcional que pide OpenRouter
+        r = self._client.post(f"{self.base_url}/chat/completions", headers=headers, json=body)
+        if (r.status_code == 429 and "daily" in r.text.lower()) or r.status_code in (402, 403):
+            # 402/403 en OpenRouter = key sin crédito o fuera de su tope: se pasa al siguiente modelo y, si
+            # todos fallan, el runner corta limpio (status quota_exhausted) en vez de grabar 300 pares "error"
+            raise DailyQuotaExhausted(f"{model}: HTTP {r.status_code} {r.text[:120]}")
+        r.raise_for_status()
+        data = r.json()
+        text = data["choices"][0]["message"]["content"] or ""
+        usage = data.get("usage", {})
+        return LLMResponse(text, model, usage.get("prompt_tokens", 0), usage.get("completion_tokens", 0), cost_usd=float(usage.get("cost") or 0.0))

ragsolver/logging/jsonl_writer.py

@@ -0,0 +1,40 @@
+"""Escritor de traza JSONL (RNF-5, docs/PLAN_RAG.md §7.6).
+
+Un archivo por corrida (`run_id`), un evento por línea. `append_event` es la
+única función que necesita el resto del código: no hay clase, no hay estado
+oculto más allá del path del archivo — ponytail: no crear un logger genérico
+para un único formato de evento.
+"""
+
+from __future__ import annotations
+
+import json
+import threading
+from pathlib import Path
+
+from ragsolver.rag.schema import TraceEvent
+
+
+def trace_path(run_id: str, base_dir: str | Path = "data/eval/traces") -> Path:
+    base = Path(base_dir)
+    base.mkdir(parents=True, exist_ok=True)
+    return base / f"{run_id}.jsonl"
+
+
+_LOCK = threading.Lock()
+
+
+def append_event(event: TraceEvent, base_dir: str | Path = "data/eval/traces") -> Path:
+    """Serializa `event` como una línea JSON y la agrega al archivo de la corrida."""
+    path = trace_path(event.run_id, base_dir)
+    with _LOCK, path.open("a", encoding="utf-8") as f:
+        f.write(event.model_dump_json() + "\n")
+    return path
+
+
+def read_events(run_id: str, base_dir: str | Path = "data/eval/traces") -> list[TraceEvent]:
+    path = trace_path(run_id, base_dir)
+    if not path.exists():
+        return []
+    with path.open(encoding="utf-8") as f:
+        return [TraceEvent.model_validate(json.loads(line)) for line in f if line.strip()]

ragsolver/orchestrator/graph.py

@@ -0,0 +1,715 @@
+"""Orquestador (docs/PLAN_RAG.md §5.3, Fase 4; propuesta §6.1-6.2; docs/PLAN_MEJORA_RAG.md §4).
+
+PROVE (demostrador local, 0 API) -> [DRAFT: plan + prueba informal de la API en el prompt del demostrador]
+-> (si `prover.api_fallback` o no hay demostrador) PLAN -> RETRIEVE -> GENERATE -> FORMALIZE -> [CLOSE -> FILL]
+-> VERIFY -> (DONE | CRITIQUE -> retry/replan/fail)
+
+Con `goal_mode` (por defecto) el Autoformalizador escribe un esqueleto `have … := by sorry`; CLOSE
+obtiene del REPL el goal de cada `sorry`, recupera premisas PARA ESE GOAL (rag/premises.py) y prueba
+una batería de tácticas con ellas (0 LLM); FILL (1 llamada) sólo ve los goals que quedaron abiertos.
+Los goals cerrados quedan en `proved` y se reutilizan en reintentos y replans (D5 del plan).
+
+LangGraph `StateGraph` sobre un dict. El estado lleva `evidence` (citas
+consultadas, §6.4), la recuperación por subobjetivo y contadores de presupuesto
+(RNF-3: `llm_budget` llamadas por problema). El retriever cuesta 0 llamadas.
+Sin checkpointer persistente (ponytail: MemorySaver/SQLite cuando haga falta
+reanudar corridas largas).
+"""
+
+from __future__ import annotations
+
+import re
+import time
+from typing import Any, TypedDict
+
+from langgraph.graph import END, START, StateGraph
+
+from ragsolver.agents.agents import Agents, InvalidLLMOutput
+from ragsolver.agents.schemas import CriticOutput, FillOutput, Problem, SolutionReport, Verdict
+from ragsolver.lean.verify import LeanChecker, build_file, count_sorries, fill_sorries, identifiers_used, skeletonize, verify
+from ragsolver.llm import DailyQuotaExhausted
+from ragsolver.prover import ProverUnavailable, draft_hint, examples_hint, extract_tactics, goal_to_theorem, prove as prover_prove, renamed_inaccessible
+from ragsolver.rag import premises as P
+from ragsolver.rag.proofs import similar as similar_proofs
+from ragsolver.rag.retrieve import Retriever
+from ragsolver.rag.schema import Citation, Hit, RetrievalRequest
+
+
+class State(TypedDict, total=False):
+    problem: Problem
+    cfg: dict
+    run_id: str
+    exemplars: list[Hit]
+    plan: Any
+    lemmas: list[Hit]
+    evidence: dict[str, Citation]
+    citation_ids: dict[str, str]
+    sketch: str
+    used_citations: list[str]
+    proof_tactics: str
+    lean_code: str
+    verdict: Verdict | None
+    lean_error: str
+    feedback: str
+    missing_identifiers: list[str]
+    attempt: int
+    replans: int
+    history: list[dict]
+    error_types: list[str]
+    re_retrievals: int
+    re_retrievals_ok: int
+    llm_calls: int
+    retrieval_calls: int
+    tokens_in: int
+    tokens_out: int
+    models: list[str]
+    status: str
+    fail_reason: str
+    t0: float
+    skeleton: str
+    candidates: list  # bloque del LLM para cada `sorry` del esqueleto (None = sin candidato)
+    goals: list[dict]  # [{goal, proof_state, block, premises}] del esqueleto actual
+    proved: dict[str, str]  # goal normalizado -> bloque que lo cerró (se conserva entre intentos y replans)
+    prover_samples: int
+    solved_by: str
+
+
+def _count(state: State, resp) -> dict:
+    return {
+        "llm_calls": state.get("llm_calls", 0) + getattr(resp, "calls", 1),
+        "tokens_in": state.get("tokens_in", 0) + resp.tokens_in,
+        "tokens_out": state.get("tokens_out", 0) + resp.tokens_out,
+        "models": list(dict.fromkeys(state.get("models", []) + [resp.model])),
+    }
+
+
+# lo que REPAIR y SKETCH conservan de un CLOSE que no terminó la prueba: pasos probados y contabilidad
+_CLOSE_KEEP = ("proved", "prover_samples", "evidence", "citation_ids", "lemmas", "retrieval_calls")
+
+
+def _over_budget(state: State) -> bool:
+    return state.get("llm_calls", 0) >= state["cfg"]["llm_budget"]
+
+
+def _format_error(verdict: Verdict) -> str:
+    return "\n".join(f"line {e['line']}:{e['col']}: {e['message']}" for e in verdict.errors)[:3000] or ("uses sorry" if verdict.uses_sorry else "unknown error")
+
+
+def _assign_citation_ids(state: State, hits: list[Hit], prefix: str) -> dict[str, str]:
+    """BUG-1: mapa `chunk_id -> citation_id` estable durante todo el problema —
+    reutiliza el id ya asignado a un chunk que vuelve a aparecer (tras un replan
+    o una re-recuperación) y sólo asigna el siguiente número libre del prefijo a
+    los chunks nuevos. Antes `retrieve()` renumeraba `M1..Mn` en cada llamada:
+    un chunk que ya estaba en `evidence` con `M3` podía volver a verse como `M1`
+    en la siguiente búsqueda, y el `M1` real quedaba duplicado (34/300 reportes
+    de `eval_v1` con `citation_id` repetidos, afectando `used_in_sketch`)."""
+    ids = dict(state.get("citation_ids", {}))
+    next_n = max((int(v[len(prefix):]) for v in ids.values() if v.startswith(prefix) and v[len(prefix):].isdigit()), default=0) + 1
+    for h in hits:
+        if h.chunk_id not in ids:
+            ids[h.chunk_id] = f"{prefix}{next_n}"
+            next_n += 1
+        h.citation.citation_id = ids[h.chunk_id]
+    return ids
+
+
+def _goal_key(goal: str) -> str:
+    return " ".join(goal.split())
+
+
+def render_tactic(entry: dict, use_rag: bool, premises: list[str], hints: list[str]) -> str | None:
+    """Táctica de la batería CLOSE para una entrada de `close.tactics` (None = se omite)."""
+    if not use_rag:
+        return entry.get("plain")
+    tac = entry["rag"]
+    if ("{premises}" in tac and not premises) or ("{hints}" in tac and not hints):
+        return entry.get("plain")
+    return tac.replace("{premises}", ", ".join(premises)).replace("{hints}", ", ".join(hints))
+
+
+def concrete_block(tactic: str, infos: list[str]) -> str:
+    """`try?` cierra el goal y sugiere el script concreto ("Try this: [apply] exact …"): ese script es
+    el que va al archivo final, para que el kernel nunca acepte una táctica con `?`."""
+    if not tactic.rstrip().endswith("?"):
+        return tactic
+    for info in infos:
+        for line in info.splitlines():
+            line = line.strip()
+            if line.startswith("[apply] "):
+                return line[len("[apply] "):]
+    return tactic
+
+
+def close_goal(checker: LeanChecker, goal: dict, tactics: list[dict], use_rag: bool, premises: list[str], hints: list[str], timeout_s: float = 60, heartbeats: int | None = 200000) -> tuple[str | None, list[dict]]:
+    """Batería CLOSE sobre un goal (docs/PLAN_MEJORA_RAG.md Fase 4): la primera táctica que lo cierra
+    gana. Devuelve (bloque concreto o None, [{tactic, closed, error}])."""
+    log = []
+    for entry in tactics:
+        tac = render_tactic(entry, use_rag, premises, hints)
+        if not tac:
+            continue
+        closed, msg, infos = checker.step(goal["proof_state"], tac, timeout=timeout_s, heartbeats=heartbeats, gen=goal.get("gen"))
+        log.append({"tactic": tac[:200], "closed": closed, "error": "" if closed else msg[:300]})
+        if closed:
+            return concrete_block(tac, infos), log
+        if "stale proof state" in msg or "lean repl failure" in msg:  # el REPL se reinició: el goal queda abierto
+            break
+    return None, log
+
+
+def _premise_hit(name: str, sig: str, dense: dict[str, Hit], ctx: dict) -> Hit:
+    if name in dense:
+        return dense[name]
+    cit = Citation(citation_id="M0", chunk_id=f"mathlib:{name}:0", corpus="mathlib", unit_type="mathlib_decl", label=name, locator={"decl_name": name, "module_path": "", "docs_url": ""}, retrieved_for=ctx)
+    return Hit(chunk_id=cit.chunk_id, corpus="mathlib", unit_type="mathlib_decl", rank=1, text=f"{name} : {sig}", metadata={"decl_name": name, "signature": sig}, citation=cit)
+
+
+def select_premises(retriever: Retriever | None, goal: str, k: int = 16, n_candidates: int = 50, rerank: bool = False, ctx: dict | None = None, dense_channel: bool = False) -> tuple[list[str], dict[str, Hit]]:
+    """Premisas para un goal de Lean (docs/PLAN_MEJORA_RAG.md Fase 3): canal A (prior filtrado por los
+    símbolos del goal) y, si `dense_channel`, canal C (índice denso con la meta del goal) fusionado con
+    RRF. Devuelve (nombres, hits densos por nombre). 0 llamadas LLM.
+
+    El canal C está apagado por defecto (`close.dense_channel`, DECISIONS #98): recall@16 por goal 0.028
+    frente a 0.327 del prior, y fusionado con RRF baja el total a 0.097."""
+    a = P.prior_channel(goal, k=2 * k)
+    dense: dict[str, Hit] = {}
+    if retriever is not None and dense_channel:
+        try:
+            req = RetrievalRequest(queries=[P.goal_target(goal)[:2000] or goal[:2000]], mode="formal", corpora=["mathlib"], k=k, n_candidates=n_candidates, rerank=rerank, include_figures=False, context=ctx or {"problem_id": "", "agent": "close"})
+            dense = {h.metadata.get("decl_name"): h for h in retriever.search(req).hits if h.metadata.get("decl_name")}
+        except Exception:  # sin índice denso (tests, demo sin tabla): sólo el prior
+            pass
+    return P.fuse(a, list(dense), k=k), dense
+
+
+class Orchestrator:
+    def __init__(self, agents: Agents, retriever: Retriever | None, checker: LeanChecker | None = None, prover=None, drafter: Agents | None = None):
+        self.agents = agents
+        self.retriever = retriever
+        self.checker = checker  # None -> un proceso `lake env lean` por verificación
+        self.prover = prover  # demostrador local (ragsolver.prover.LocalProver) o None
+        self.drafter = drafter  # Agents con el LLM que escribe el borrador de DRAFT (`llm_draft`, con razonamiento); None = `agents`
+        self.graph = self._build()
+
+    # -- nodos ---------------------------------------------------------------------
+
+    def _prover_cfg(self, state: State) -> dict | None:
+        pcfg = state["cfg"].get("prover") or {}
+        return pcfg if pcfg.get("enabled") and self.prover is not None and self.checker is not None else None
+
+    def _api_loop(self, state: State) -> bool:
+        """¿Corre el bucle de agentes por API (PLAN → … → CRITIQUE) cuando el demostrador no resuelve? Sin
+        demostrador, siempre; con él, sólo si `prover.api_fallback` (en eval-v3 costó US$0.06 en los 9
+        problemas que el demostrador no resolvió y no resolvió ninguno)."""
+        pcfg = self._prover_cfg(state)
+        return pcfg is None or bool(pcfg.get("api_fallback", True))
+
+    def prove(self, state: State) -> dict:
+        """Etapa 0 (docs/PLAN_REDISENO_PROVER.md): el demostrador local intenta el teorema completo, 0 API.
+        Con RAG, la autocorrección recibe nombres que existen en el Mathlib fijado (se citan)."""
+        pcfg = self._prover_cfg(state)
+        if pcfg is None:
+            return {}
+        cfg, problem = state["cfg"], state["problem"]
+        name = re.match(r"\s*(?:theorem|lemma)\s+(\S+)", problem.formal_statement)
+        if not name:
+            return {}
+        retr = self.retriever if cfg["rag"] and pcfg.get("rag_names") else None
+        tac, log = prover_prove(self.prover, self.checker, problem.formal_statement, problem.header, name.group(1), k=pcfg["k_root"], correction_rounds=pcfg.get("correction_rounds", 1), retriever=retr, max_heartbeats=cfg["lean"]["max_heartbeats"])
+        self.agents.trace("prover", state["run_id"], problem.problem_id, 1, log.get("seconds", 0) * 1000, {"stage": "root", "solved": bool(tac), **{k: v for k, v in log.items() if k not in ("suggested", "candidates")}, "suggested": list(log.get("suggested", {}))})
+        delta = self._cite(state, log.get("suggested", {}), "prover")
+        delta["prover_samples"] = state.get("prover_samples", 0) + log["samples"] + log["rounds"] * 2
+        if tac:
+            delta.update(proof_tactics=tac, solved_by="prover_root")
+            return delta
+        if pcfg.get("examples") and cfg["rag"]:
+            delta.update(self.examples({**state, **delta}, name.group(1), pcfg))
+        if pcfg.get("repair") and not delta.get("solved_by"):
+            delta.update(self.repair({**state, **delta}, log.get("candidates", []), pcfg["repair"]))
+        if pcfg.get("sketch") and not delta.get("solved_by"):
+            delta.update(self.sketch({**state, **delta}, name.group(1), pcfg["sketch"]))
+        if not delta.get("solved_by") and not pcfg.get("dsp") and not self._api_loop(state):
+            delta.update(status="fail", fail_reason="prover: sin prueba (respaldo por API apagado: prover.api_fallback)")
+        return delta
+
+    def examples(self, state: State, name: str, pcfg: dict) -> dict:
+        """EXAMPLES (`prover.examples`, RAG de pruebas, `rag/proofs.py`): si la etapa 0 falla, las pruebas
+        verificadas de los `examples` problemas más parecidos (embeddings sobre Lean Workbook) (1) se prueban tal
+        cual sobre el enunciado (0 GPU: la misma táctica a veces cierra un problema análogo) y (2) van como
+        ejemplos en el prompt del demostrador (`k_examples` muestras, como DRAFT; su control es
+        `baseline_prover16`)."""
+        cfg, problem = state["cfg"], state["problem"]
+        t0 = time.time()
+        hits = similar_proofs(f"{problem.informal_statement}\n{problem.formal_statement}", k=pcfg["examples"], max_sim=pcfg.get("max_sim", 0.95))
+        info = {"stage": "examples", "retrieved": [(h["problem_id"], h["sim"]) for h in hits]}
+        delta = {"retrieval_calls": state.get("retrieval_calls", 0) + 1}
+        for h in hits:
+            if self.checker.check(problem.formal_statement, h["proof"], problem.header, cfg["lean"]["max_heartbeats"]).ok:
+                self.agents.trace("prover", state["run_id"], problem.problem_id, 1, (time.time() - t0) * 1000, {**info, "solved": True, "solved_in": f"direct:{h['problem_id']}"})
+                return {**delta, "proof_tactics": h["proof"], "solved_by": "prover_examples"}
+        if not hits:
+            return delta
+        tac, log = prover_prove(self.prover, self.checker, problem.formal_statement, problem.header, name, k=pcfg.get("k_examples", 8), correction_rounds=0, max_heartbeats=cfg["lean"]["max_heartbeats"], hint=examples_hint(hits))
+        self.agents.trace("prover", state["run_id"], problem.problem_id, 1, (time.time() - t0) * 1000, {**info, "solved": bool(tac), **{k: v for k, v in log.items() if k not in ("suggested", "candidates")}})
+        delta["prover_samples"] = state.get("prover_samples", 0) + log["samples"]
+        if tac:
+            delta.update(proof_tactics=tac, solved_by="prover_examples")
+        return delta
+
+    def repair(self, state: State, candidates: list[str], n: int) -> dict:
+        """REPAIR (0 API, `prover.repair`): una prueba fallida del demostrador suele tener casi todos los pasos
+        bien. Se parte en sus `have` como la del Formalizador (`skeletonize`) y pasa por CLOSE: el bloque del
+        propio demostrador primero, la batería y el demostrador sobre el lema corto sólo en los pasos que fallan.
+        Se prueban las `n` mejores (menos errores de Lean) cuyo esqueleto elabora; lo probado queda en `proved`."""
+        keep: dict = {}
+        tried = 0
+        for tac in candidates:
+            if tried >= n:
+                break
+            skeleton, cands = skeletonize(tac)
+            if count_sorries(skeleton) < 2:  # sin `have` no hay nada que partir: es la misma prueba que ya falló
+                continue
+            d = self.close({**state, **keep, "skeleton": skeleton, "candidates": cands})
+            keep.update({k: d[k] for k in _CLOSE_KEEP if k in d})
+            if not d.get("goals"):  # el esqueleto no elabora (falla el cierre o la estructura): cuesta una llamada al REPL
+                continue
+            tried += 1
+            if "proof_tactics" in d:
+                return {**keep, "proof_tactics": d["proof_tactics"], "solved_by": "prover_repair"}
+        return keep
+
+    def sketch(self, state: State, name: str, rounds: int) -> dict:
+        """SKETCH (`prover.sketch` rondas; receta de DeepSeek-Prover-V2): el modelo con razonamiento (`llm_draft`)
+        escribe el esqueleto en Lean, pasos `have … := by sorry`; CLOSE cierra cada paso con la batería y el
+        demostrador sobre el lema corto. Si quedan pasos abiertos, la ronda siguiente le muestra cuáles para que
+        los parta más; si el esqueleto no elabora, el error de Lean."""
+        delta: dict = {}
+        feedback = ""
+        for rnd in range(rounds):
+            if _over_budget({**state, **delta}):
+                break
+            text, resp = (self.drafter or self.agents).sketch(state["problem"], feedback, state["run_id"], rnd + 1)
+            delta.update(_count({**state, **delta}, resp))
+            tac = extract_tactics(text, name)
+            if not tac:
+                feedback = f"Your answer had no ```lean4 block with `theorem {name}`."
+                continue
+            skeleton, cands = skeletonize(tac)
+            d = self.close({**state, **delta, "skeleton": skeleton, "candidates": cands})
+            delta.update({k: d[k] for k in _CLOSE_KEEP if k in d})
+            if "proof_tactics" in d:
+                return {**delta, "proof_tactics": d["proof_tactics"], "solved_by": "prover_sketch"}
+            if not d.get("goals"):
+                feedback = f"Previous skeleton:\n{tac[:3000]}\nIt does not compile in Lean:\n{d.get('lean_error', '')[:1500]}"
+            else:
+                open_ = "\n\n".join(g["goal"] for g in d["goals"] if not g.get("block"))
+                feedback = f"Previous skeleton:\n{tac[:3000]}\nNo automation could prove these steps (Lean goals). Split them into smaller `have` steps or use another argument:\n{open_[:3000]}"
+        return delta
+
+    def draft(self, state: State) -> dict:
+        """DRAFT (Draft-Sketch-Prove, `prover.dsp`): si la etapa 0 no resolvió, el modelo de la API escribe el
+        plan y la prueba informal (Planificador + Generador, 2 llamadas) y el demostrador local recibe eso,
+        junto con los lemas del RAG para el goal raíz, DENTRO de su prompt (`k_draft` muestras). Es el lugar
+        donde la API y el RAG pueden mover la prueba: el demostrador sabe Lean y el modelo general razona en
+        lenguaje natural."""
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget"}
+        pcfg, cfg, problem = self._prover_cfg(state), state["cfg"], state["problem"]
+        agents = self.drafter or self.agents
+        exemplars, delta = self._exemplars(state)
+        plan, r1 = agents.plan(problem, exemplars, state["run_id"], 1)
+        delta.update(plan=plan, exemplars=exemplars, **_count(state, r1))
+        out, r2 = agents.generate(problem, plan, [], exemplars, "", state["run_id"], 1)
+        delta.update(sketch=out.sketch, used_citations=out.used_citations, **_count({**state, **delta}, r2))
+        lemmas: dict[str, str] = {}
+        if cfg["rag"]:  # canal A (prior de competición) sobre el goal raíz, con su firma
+            goals, errors = self.checker.goals(problem.formal_statement, "sorry", problem.header, cfg["lean"]["max_heartbeats"])
+            if len(goals) == 1 and not errors:
+                prior = {r["decl_name"]: r.get("type", "") for r in P.load_prior()}
+                lemmas = {n: prior.get(n, "") for n in P.prior_channel(goals[0]["goal"], k=pcfg.get("k_lemmas", 10))}
+        hint = draft_hint(plan.strategy, [s.statement_nl for s in plan.subgoals], out.sketch, lemmas)
+        name = re.match(r"\s*(?:theorem|lemma)\s+(\S+)", problem.formal_statement).group(1)
+        tac, log = prover_prove(self.prover, self.checker, problem.formal_statement, problem.header, name, k=pcfg.get("k_draft", 8), correction_rounds=0, max_heartbeats=cfg["lean"]["max_heartbeats"], hint=hint)
+        self.agents.trace("prover", state["run_id"], problem.problem_id, 1, log.get("seconds", 0) * 1000, {"stage": "draft", "solved": bool(tac), "lemmas": list(lemmas), **{k: v for k, v in log.items() if k not in ("suggested", "candidates")}})
+        delta.update(self._cite({**state, **delta}, lemmas, "prover"))
+        delta["prover_samples"] = state.get("prover_samples", 0) + log["samples"]
+        if tac:
+            delta.update(proof_tactics=tac, solved_by="prover_draft")
+        elif not self._api_loop(state):
+            delta.update(status="fail", fail_reason="prover: sin prueba tras DRAFT (respaldo por API apagado: prover.api_fallback)")
+        return delta
+
+    def _exemplars(self, state: State) -> tuple[list[Hit], dict]:
+        """Ejemplares del corpus informal para el Planificador (0 LLM) y su delta de citas/evidencia."""
+        cfg, problem = state["cfg"], state["problem"]
+        exemplars: list[Hit] = []
+        searched = cfg["rag"] and "informal" in cfg["corpora"] and self.retriever is not None
+        if searched:
+            req = RetrievalRequest(queries=[problem.informal_statement[:2000]], mode="exemplar", corpora=["informal"], k=cfg["retrieval"]["k_informal"], n_candidates=cfg["retrieval"]["n_candidates"], rerank=cfg["retrieval"]["rerank"], context={"problem_id": problem.problem_id, "subgoal_id": "", "attempt": state.get("attempt", 1), "agent": "planner", "run_id": state["run_id"]})
+            exemplars = self.retriever.search(req).hits
+        citation_ids = _assign_citation_ids(state, exemplars, "I")
+        evidence = dict(state.get("evidence", {}))
+        for h in exemplars:
+            evidence.setdefault(h.chunk_id, h.citation)
+        return exemplars, {"evidence": evidence, "citation_ids": citation_ids, "retrieval_calls": state.get("retrieval_calls", 0) + int(searched)}
+
+    def _cite(self, state: State, suggested: dict[str, str], agent: str) -> dict:
+        """Nombres que propuso el RAG (sugerencias de la autocorrección) como citas `M*`."""
+        if not suggested:
+            return {}
+        ctx = {"problem_id": state["problem"].problem_id, "subgoal_id": "", "attempt": state.get("attempt", 1), "agent": agent, "run_id": state["run_id"]}
+        hits = [_premise_hit(n, sig, {}, ctx) for n, sig in suggested.items()]
+        evidence = dict(state.get("evidence", {}))
+        ids = _assign_citation_ids(state, hits, "M")
+        for h in hits:
+            evidence.setdefault(h.chunk_id, h.citation)
+        return {"evidence": evidence, "citation_ids": ids}
+
+    def plan(self, state: State) -> dict:
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget"}
+        problem = state["problem"]
+        exemplars, ex_delta = self._exemplars(state)
+        feedback = ""
+        if state.get("plan") is not None:  # replan (DES-1): razón del Crítico + plan anterior + lo ya probado
+            proved = [P.goal_target(k) for k in state.get("proved", {})]
+            feedback = f"Critic: {state.get('feedback', '')}\nPrevious strategy: {state['plan'].strategy}" + ("\nAlready proved (reuse as facts):\n" + "\n".join(f"- {t}" for t in proved) if proved else "")
+        plan, resp = self.agents.plan(problem, exemplars, state["run_id"], state.get("attempt", 1), feedback=feedback)
+        return {"exemplars": exemplars, "plan": plan, "feedback": "", "solved_by": "", **ex_delta, **_count(state, resp)}
+
+    def retrieve(self, state: State) -> dict:
+        cfg, problem = state["cfg"], state["problem"]
+        if not cfg["rag"] or self.retriever is None:
+            return {"lemmas": [], "missing_identifiers": []}
+        hits: dict[str, Hit] = {}
+        k = cfg["retrieval"]["k_mathlib"]
+        ctx = lambda sg, agent: {"problem_id": problem.problem_id, "subgoal_id": sg, "attempt": state.get("attempt", 1), "agent": agent, "run_id": state["run_id"]}
+        re_ok, re_n = state.get("re_retrievals_ok", 0), state.get("re_retrievals", 0)
+        n_calls = state.get("retrieval_calls", 0)
+        missing = state.get("missing_identifiers", [])
+        if missing:  # re-recuperación tras `lema faltante` (0 llamadas LLM)
+            re_n += 1
+            queries = [f"unknown identifier '{m}'" for m in missing[:3]] + [state.get("lean_error", "")[:500] or problem.formal_statement[:500]]
+            res = self.retriever.search(RetrievalRequest(queries=queries[:4], mode="error", corpora=["mathlib"], k=k, n_candidates=cfg["retrieval"]["n_candidates"], rerank=cfg["retrieval"]["rerank"], context=ctx("", "critic")))
+            n_calls += 1
+            if any(h.metadata.get("decl_name") in missing for h in res.hits):
+                re_ok += 1
+            for h in res.hits:
+                hits.setdefault(h.chunk_id, h)
+        for sg in [] if cfg.get("goal_mode") and self.checker is not None else state["plan"].subgoals:  # goal_mode: las premisas se recuperan por goal en CLOSE
+            queries = ([sg.statement_nl] + list(sg.search_queries))[:4]
+            res = self.retriever.search(RetrievalRequest(queries=queries, mode="nl", corpora=["mathlib"], k=k, n_candidates=cfg["retrieval"]["n_candidates"], rerank=cfg["retrieval"]["rerank"], rerank_against=sg.statement_nl, context=ctx(sg.subgoal_id, "retriever")))
+            n_calls += 1
+            for h in res.hits:
+                hits.setdefault(h.chunk_id, h)
+        lemmas = list(hits.values())
+        citation_ids = _assign_citation_ids(state, lemmas, "M")
+        evidence = dict(state.get("evidence", {}))
+        for h in lemmas:
+            evidence.setdefault(h.chunk_id, h.citation)
+        return {"lemmas": lemmas, "evidence": evidence, "citation_ids": citation_ids, "missing_identifiers": [], "re_retrievals": re_n, "re_retrievals_ok": re_ok, "retrieval_calls": n_calls}
+
+    def generate(self, state: State) -> dict:
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget"}
+        out, resp = self.agents.generate(state["problem"], state["plan"], state.get("lemmas", []), state.get("exemplars", []), state.get("feedback", ""), state["run_id"], state.get("attempt", 1))
+        return {"sketch": out.sketch, "used_citations": out.used_citations, **_count(state, resp)}
+
+    def formalize(self, state: State) -> dict:
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget"}
+        goal_mode = bool(state["cfg"].get("goal_mode")) and self.checker is not None
+        proved = [f"have : {P.goal_target(k)} := by {b}" for k, b in state.get("proved", {}).items()]
+        out, resp = self.agents.formalize(state["problem"], state["sketch"], state.get("lemmas", []), state.get("lean_error", ""), state["run_id"], state.get("attempt", 1), skeleton=goal_mode, proved=proved)
+        if goal_mode:  # la prueba del modelo se parte en goals; sus bloques son el primer candidato de cada uno
+            skeleton, candidates = skeletonize(out.proof_tactics)
+            return {"skeleton": skeleton, "candidates": candidates, "proof_tactics": skeleton, **_count(state, resp)}
+        lean = state["cfg"]["lean"]
+        problem = state["problem"]
+        # BUG-2: `lean_code` reportado == lo que verifica `verify()` (mismo `theorem_block`, mismos `open`).
+        code = build_file(problem.formal_statement, out.proof_tactics, lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+        return {"proof_tactics": out.proof_tactics, "lean_code": code, **_count(state, resp)}
+
+    def close(self, state: State) -> dict:
+        """CLOSE (0 LLM): goals del esqueleto -> premisas por goal -> batería de tácticas."""
+        cfg, problem = state["cfg"], state["problem"]
+        lean, ccfg = cfg["lean"], cfg["close"]
+        skeleton = state["skeleton"]
+        goals, errors = self.checker.goals(problem.formal_statement, skeleton, problem.header, lean["max_heartbeats"])
+        n_tokens = count_sorries(skeleton)
+        if errors or len(goals) != n_tokens:
+            msg = "\n".join(f"line {e['line']}:{e['col']}: {e['message']}" for e in errors) or f"the skeleton has {n_tokens} `sorry` but Lean found {len(goals)} goals: use exactly one `sorry` per goal"
+            self.agents.trace("close", state["run_id"], problem.problem_id, state.get("attempt", 1), 0, {"skeleton_ok": False, "error": msg[:300]})
+            code = build_file(problem.formal_statement, skeleton, lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+            return {"goals": [], "lean_error": msg[:3000], "lean_code": code, "verdict": Verdict(ok=False, errors=errors or [{"line": 0, "col": 0, "message": msg}])}
+        use_rag = bool(cfg["rag"]) and self.retriever is not None
+        proved = dict(state.get("proved", {}))
+        evidence = dict(state.get("evidence", {}))
+        new_hits: list[Hit] = []
+        n_calls = state.get("retrieval_calls", 0)
+        candidates = state.get("candidates") or [None] * len(goals)
+        n_prover_goals, prover_samples = 0, state.get("prover_samples", 0)
+        pcfg = self._prover_cfg(state)
+
+        def refresh() -> None:  # el REPL se reinició (timeout de este hilo o de otro): proof_state nuevos
+            fresh, errs = self.checker.goals(problem.formal_statement, skeleton, problem.header, lean["max_heartbeats"])
+            if not errs and len(fresh) == len(goals):
+                for h, f in zip(goals, fresh):
+                    h.update(proof_state=f["proof_state"], gen=f["gen"])
+
+        for i, g in enumerate(goals):
+            g["candidate"] = candidates[i] if i < len(candidates) else None
+            for _ in range(2):  # 2.º intento sólo si el REPL se reinició a mitad del goal (eval-v4: pasos "stale" sin probar)
+                if getattr(self.checker, "gen", g.get("gen")) != g.get("gen"):
+                    refresh()
+                prover_ok = pcfg is not None and n_prover_goals < pcfg.get("max_goals", 3)
+                block, names, hits, log, n = self._close_one(state, g, i, proved, use_rag, prover_ok)
+                n_calls += hits is not None
+                new_hits += hits or []
+                prover_samples += n
+                n_prover_goals += any(t["tactic"] == "prover" for t in log)
+                if block or not any("stale proof state" in t["error"] for t in log):
+                    break
+            g.update(block=block, premises=names, log=log)
+            if block:
+                proved[_goal_key(g["goal"])] = block
+            self.agents.trace("close", state["run_id"], problem.problem_id, state.get("attempt", 1), 0, {"goal": i, "closed": bool(block), "block": (block or "")[:200], "premises": names, "tried": log})
+        citation_ids = _assign_citation_ids(state, new_hits, "M")
+        for h in new_hits:
+            evidence.setdefault(h.chunk_id, h.citation)
+        delta = {"goals": goals, "prover_samples": prover_samples, "lean_error": "", "proved": proved, "evidence": evidence, "citation_ids": citation_ids, "lemmas": list({h.chunk_id: h for h in state.get("lemmas", []) + new_hits}.values()), "retrieval_calls": n_calls}
+        if all(g["block"] for g in goals):
+            delta["proof_tactics"] = fill_sorries(skeleton, [g["block"] for g in goals])
+        return delta
+
+    def _close_one(self, state: State, g: dict, i: int, proved: dict, use_rag: bool, prover_ok: bool) -> tuple[str | None, list[str], list[Hit] | None, list[dict], int]:
+        """Un goal de CLOSE: lo ya probado en un intento anterior, el bloque del modelo para ese paso, la batería
+        con las premisas del goal y, si `prover_ok`, el demostrador sobre el lema corto. Devuelve (bloque o None,
+        premisas, hits del RAG o None si no se buscó, log, muestras del demostrador)."""
+        ccfg, hb = state["cfg"]["close"], state["cfg"]["lean"]["max_heartbeats"]
+        key = _goal_key(g["goal"])
+        if key in proved:
+            closed, _msg, _ = self.checker.step(g["proof_state"], proved[key], timeout=ccfg["timeout_s"], heartbeats=hb, gen=g.get("gen"))
+            if closed:
+                return proved[key], [], None, [{"tactic": "reused", "closed": True, "error": ""}], 0
+        cand_log = []
+        if g.get("candidate"):
+            closed, msg, _ = self.checker.step(g["proof_state"], g["candidate"], timeout=ccfg["timeout_s"], heartbeats=hb, gen=g.get("gen"))
+            cand_log = [{"tactic": "llm", "closed": closed, "error": "" if closed else msg[:300]}]
+            if closed:
+                return g["candidate"], [], None, cand_log, 0
+        names, hints, hits = [], [], None
+        if use_rag:
+            names, hits = self._premises(state, g["goal"], ccfg["k_premises"], i)
+            hints = P.nlinarith_hints(g["goal"])
+        block, log = close_goal(self.checker, g, ccfg["tactics"], use_rag, names, hints, ccfg["timeout_s"])
+        n = 0
+        if block is None and prover_ok:
+            block, plog, n = self._prove_goal(state, g, i, self._prover_cfg(state))
+            log = log + plog
+        return block, names, hits, cand_log + log, n
+
+    def _prove_goal(self, state: State, g: dict, i: int, pcfg: dict) -> tuple[str | None, list[dict], int]:
+        """Un goal abierto como lema autónomo para el demostrador (receta DeepSeek-Prover-V2); el bloque se
+        acepta sólo si cierra el goal EN SU CONTEXTO (`step`), con `rename_i` para los nombres inaccesibles."""
+        name = f"rs_goal_{i}"
+        stmt = goal_to_theorem(g["goal"], name)
+        if stmt is None:
+            return None, [{"tactic": "prover", "closed": False, "error": "goal no convertible a lema"}], 0
+        problem = state["problem"]
+        tac, plog = prover_prove(self.prover, self.checker, stmt, problem.header, name, k=pcfg.get("k_goal", 2), correction_rounds=0, max_heartbeats=state["cfg"]["lean"]["max_heartbeats"])
+        n = plog["samples"]
+        if not tac:
+            return None, [{"tactic": "prover", "closed": False, "error": f"{plog['extracted']}/{n} muestras extraídas, ninguna verifica"}], n
+        renamed = renamed_inaccessible(g["goal"])
+        block = (f"rename_i {' '.join(renamed)}\n" if renamed else "") + tac
+        closed, msg, _ = self.checker.step(g["proof_state"], block, timeout=state["cfg"]["close"]["timeout_s"], heartbeats=state["cfg"]["lean"]["max_heartbeats"], gen=g.get("gen"))
+        return (block if closed else None), [{"tactic": "prover", "closed": closed, "error": "" if closed else msg[:300]}], n
+
+    def _premises(self, state: State, goal: str, k: int, i: int) -> tuple[list[str], list[Hit]]:
+        problem = state["problem"]
+        ctx = {"problem_id": problem.problem_id, "subgoal_id": f"G{i + 1}", "attempt": state.get("attempt", 1), "agent": "close", "run_id": state["run_id"]}
+        ccfg = state["cfg"]["close"]
+        names, dense = select_premises(self.retriever, goal, k, state["cfg"]["retrieval"]["n_candidates"], state["cfg"]["retrieval"]["rerank"], ctx, dense_channel=bool(ccfg.get("dense_channel")))
+        prior = {r["decl_name"]: r for r in P.load_prior()}
+        return names, [_premise_hit(n, prior.get(n, {}).get("type", ""), dense, ctx) for n in names]
+
+    def fill(self, state: State) -> dict:
+        """FILL (1 llamada): los goals que CLOSE no cerró, cada uno con su goal exacto y sus premisas."""
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget"}
+        problem, goals = state["problem"], [dict(g) for g in state["goals"]]
+        open_ = [i for i, g in enumerate(goals) if not g.get("block")]
+        sigs = {h.metadata.get("decl_name"): h.metadata.get("signature", "") for h in state.get("lemmas", [])}
+        parts = []
+        for j, i in enumerate(open_):
+            g = goals[i]
+            lem = "\n".join(f"  {n} : {sigs.get(n, '')[:300]}" for n in g.get("premises", [])) or "  (none)"
+            err = next((t["error"] for t in reversed(g.get("log", [])) if t["error"]), "")
+            prev = ""
+            if g.get("candidate"):
+                cand_err = next((t["error"] for t in g.get("log", []) if t["tactic"] == "llm"), "")
+                prev = f"\nYour previous attempt for this goal (rejected by Lean):\n{g['candidate'][:1500]}\nLean error: {cand_err[:400]}"
+            parts.append(f"[G{j + 1}]\n{g['goal']}\nLemmas:\n{lem}{prev}\nAutomation error: {err[:300] or '(none)'}")
+        try:
+            out, resp = self.agents.fill(problem, "\n\n".join(parts), state["run_id"], state.get("attempt", 1))
+        except InvalidLLMOutput as e:  # #110: sin propuestas válidas los goals siguen abiertos; no se tira el problema
+            out, resp = FillOutput(proofs=[]), e
+        by_id = {p.goal_id.strip().upper(): p.tactics for p in out.proofs}
+        proved = dict(state.get("proved", {}))
+        for j, i in enumerate(open_):
+            tac = by_id.get(f"G{j + 1}", "").strip()
+            if not tac:
+                goals[i]["block"] = "done"  # sin respuesta: el goal queda abierto y Lean lo reporta
+                continue
+            closed, msg, _ = self.checker.step(goals[i]["proof_state"], tac, timeout=state["cfg"]["close"]["timeout_s"], gen=goals[i].get("gen"))
+            goals[i]["block"] = tac
+            if closed:
+                proved[_goal_key(goals[i]["goal"])] = tac
+        return {"goals": goals, "proved": proved, "proof_tactics": fill_sorries(state["skeleton"], [g["block"] for g in goals]), **_count(state, resp)}
+
+    def verify(self, state: State) -> dict:
+        lean = state["cfg"]["lean"]
+        problem = state["problem"]
+        if self.checker is not None:
+            v = self.checker.check(problem.formal_statement, state["proof_tactics"], problem.header, lean["max_heartbeats"])
+        else:
+            v = verify(problem.formal_statement, state["proof_tactics"], f"{problem.problem_id}_a{state.get('attempt', 1)}", lean["imports"] + problem.imports, lean["timeout_s"], lean["max_heartbeats"], header=problem.header)
+        self.agents.trace("verifier", state["run_id"], problem.problem_id, state.get("attempt", 1), v.seconds * 1000, {"ok": v.ok, "uses_sorry": v.uses_sorry, "n_errors": len(v.errors), "first_error": (v.errors[0]["message"][:300] if v.errors else "")})
+        # BUG-2: `lean_code` reportado == lo verificado (en goal_mode el archivo se arma recién aquí)
+        code = build_file(problem.formal_statement, state["proof_tactics"], lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+        if v.ok:
+            return {"verdict": v, "status": "done", "lean_error": "", "lean_code": code, "solved_by": state.get("solved_by") or "agents"}
+        return {"verdict": v, "lean_error": _format_error(v), "lean_code": code}
+
+    def critique(self, state: State) -> dict:
+        cfg = state["cfg"]
+        attempt = state.get("attempt", 1)
+        history = list(state.get("history", []))
+        if cfg["k_max"] <= 1:  # ablación "sin Crítico": un solo intento, sin llamada
+            history.append({"attempt": attempt, "error_type": "unknown", "summary": state["lean_error"][:200]})
+            return {"status": "fail", "fail_reason": "exhausted", "history": history, "error_types": state.get("error_types", []) + ["unknown"]}
+        if _over_budget(state):
+            return {"status": "fail", "fail_reason": "budget", "history": history}
+        try:
+            out, resp = self.agents.critique(state["problem"], state["sketch"], state["lean_code"], state["lean_error"], history, state["run_id"], attempt)
+        except InvalidLLMOutput as e:  # #110: crítica ilegible -> reintento con los errores de Lean como feedback
+            out, resp = CriticOutput(error_type="unknown", action="retry", feedback=f"Fix the Lean errors:\n{state['lean_error'][:1500]}"), e
+        history.append({"attempt": attempt, "error_type": out.error_type, "action": out.action, "summary": out.feedback[:300]})
+        error_types = state.get("error_types", []) + [out.error_type]
+        delta = {"history": history, "error_types": error_types, "feedback": out.feedback, "missing_identifiers": out.missing_identifiers, "attempt": attempt + 1, **_count(state, resp)}
+        if out.action == "abandon":
+            return {**delta, "status": "fail", "fail_reason": "abandon"}
+        if attempt + 1 > cfg["k_max"]:
+            return {**delta, "status": "fail", "fail_reason": "exhausted"}
+        if out.action == "replan":
+            if state.get("replans", 0) >= cfg["max_replans"]:
+                return {**delta, "status": "fail", "fail_reason": "exhausted"}
+            return {**delta, "replans": state.get("replans", 0) + 1, "status": "replan"}
+        return {**delta, "status": "retry"}
+
+    # -- grafo -------------------------------------------------------------------
+
+    @staticmethod
+    def _guard(node):
+        """JSON inválido tras el reintento (`InvalidLLMOutput`) = el intento termina en fallo dentro del
+        grafo, conservando lo acumulado (llamadas, tokens, evidencia, historial). Antes la excepción
+        salía de `invoke` y el reporte perdía todo lo anterior (DECISIONS #61).
+
+        ACC-1: cualquier OTRA excepción (un bug, el REPL de Lean, la red) se captura igual, a nivel de
+        nodo — el estado acumulado hasta ese punto ya está fusionado por LangGraph y no se pierde,
+        a diferencia del `except Exception` que tenía `solve()` antes, que reemplazaba todo el estado
+        final por `{**init, "fail_reason": ...}` y descartaba llamadas/tokens/evidencia ya generados."""
+
+        def guarded(state: State) -> dict:
+            try:
+                return node(state)
+            except InvalidLLMOutput as e:  # e lleva tokens_in/tokens_out/calls/model, como una respuesta
+                return {"status": "fail", "fail_reason": f"llm_output_invalid:{e.agent}", **_count(state, e)}  # `report` lo agrega a error_types
+            except (DailyQuotaExhausted, ProverUnavailable):
+                raise  # sin modelos disponibles hoy o sin demostrador: debe salir para que el runner corte la corrida y reanude mañana
+            except Exception as e:
+                return {"status": "error", "fail_reason": f"exception: {type(e).__name__}: {str(e)[:300]}"}
+
+        return guarded
+
+    def _build(self):
+        g = StateGraph(State)
+        for name in ("prove", "draft", "plan", "retrieve", "generate", "formalize", "close", "fill", "verify", "critique"):
+            g.add_node(name, self._guard(getattr(self, name)))
+        g.add_edge(START, "prove")
+        g.add_conditional_edges("prove", lambda s: "end" if s.get("status") in ("fail", "error") else ("verify" if s.get("solved_by") in ("prover_root", "prover_examples", "prover_repair", "prover_sketch") else ("draft" if (self._prover_cfg(s) or {}).get("dsp") else "plan")), {"verify": "verify", "draft": "draft", "plan": "plan", "end": END})
+        g.add_conditional_edges("draft", lambda s: "end" if s.get("status") in ("fail", "error") else ("verify" if s.get("solved_by") == "prover_draft" else "plan"), {"verify": "verify", "plan": "plan", "end": END})
+        g.add_conditional_edges("plan", lambda s: "end" if s.get("status") in ("fail", "error") else "retrieve", {"retrieve": "retrieve", "end": END})
+        g.add_conditional_edges("retrieve", lambda s: "end" if s.get("status") == "error" else "generate", {"generate": "generate", "end": END})
+        g.add_conditional_edges("generate", lambda s: "end" if s.get("status") in ("fail", "error") else "formalize", {"formalize": "formalize", "end": END})
+        g.add_conditional_edges("formalize", lambda s: "end" if s.get("status") in ("fail", "error") else ("close" if s.get("skeleton") is not None and s["cfg"].get("goal_mode") and self.checker is not None else "verify"), {"close": "close", "verify": "verify", "end": END})
+        # CLOSE: esqueleto que no elabora -> Crítico; todo cerrado -> VERIFY; quedan goals -> FILL
+        g.add_conditional_edges("close", lambda s: "end" if s.get("status") == "error" else ("critique" if not s.get("goals") and s.get("lean_error") else ("verify" if all(x.get("block") for x in s.get("goals", [])) else "fill")), {"critique": "critique", "verify": "verify", "fill": "fill", "end": END})
+        g.add_conditional_edges("fill", lambda s: "end" if s.get("status") in ("fail", "error") else "verify", {"verify": "verify", "end": END})
+        # si la etapa 0 dio una prueba que VERIFY no acepta (no debería: ya pasó `check`), siguen los agentes
+        g.add_conditional_edges("verify", lambda s: "end" if s.get("status") in ("done", "error") or not self._api_loop(s) else ("plan" if s.get("solved_by") in ("prover_root", "prover_examples", "prover_repair", "prover_sketch", "prover_draft") and not s.get("history") else "critique"), {"critique": "critique", "plan": "plan", "end": END})
+        g.add_conditional_edges(
+            "critique",
+            lambda s: {"retry": ("retrieve" if s.get("missing_identifiers") else "generate"), "replan": "plan"}.get(s.get("status"), "end"),
+            {"retrieve": "retrieve", "generate": "generate", "plan": "plan", "end": END},
+        )
+        return g.compile()
+
+    def solve(self, problem: Problem, cfg: dict, run_id: str) -> SolutionReport:
+        t0 = time.time()
+        if problem.imports:  # nadie usa imports adicionales por problema hoy (auditoría BUG-4); error explícito en vez de ignorarlos en silencio
+            return self.report(problem, cfg, {"fail_reason": f"unsupported: Problem.imports no soportado: {problem.imports}"}, "fail", 0.0)
+        init: State = {"problem": problem, "cfg": cfg, "run_id": run_id, "attempt": 1, "replans": 0, "evidence": {}, "history": [], "error_types": [], "llm_calls": 0, "retrieval_calls": 0, "tokens_in": 0, "tokens_out": 0, "models": [], "status": "running", "lean_error": "", "feedback": "", "missing_identifiers": []}
+        try:
+            final = self.graph.invoke(init, config={"recursion_limit": 60})
+            # ACC-1: "error" (excepción capturada dentro de un nodo, ver `_guard`) es un estado
+            # terminal distinto de "fail" (el grafo llegó a FAIL de forma normal); cualquier otro
+            # valor (no debería darse aquí) cae a "fail" por seguridad.
+            status = final.get("status") if final.get("status") in ("done", "error") else "fail"
+        except (DailyQuotaExhausted, ProverUnavailable):
+            raise  # sin modelos disponibles hoy o sin demostrador: el runner corta la corrida y se reanuda mañana
+        except Exception as e:  # red de seguridad final: no debería alcanzarse con _guard ya en cada nodo
+            final, status = {**init, "fail_reason": f"exception: {type(e).__name__}: {str(e)[:300]}"}, "error"
+        return self.report(problem, cfg, final, status, time.time() - t0)
+
+    @staticmethod
+    def report(problem: Problem, cfg: dict, final: dict, status: str, wall: float) -> SolutionReport:
+        used_ids = set(final.get("used_citations", []))
+        proof = final.get("proof_tactics", "") if status == "done" else ""
+        # `used_in_proof`: la constante está en el término que aceptó el kernel (REPL). Nombrarla en el texto no
+        # basta: `grind +lax [16 lemas]` nombra 16 y usa uno o dos (smoke 2026-10-14, DECISIONS #101). Sin esa
+        # información (backend `lake`), el criterio textual de antes.
+        verdict = final.get("verdict")
+        used_consts = set(verdict.used_constants) if status == "done" and verdict is not None and verdict.used_constants else None
+        citations = []
+        for c in final.get("evidence", {}).values():
+            c = c.model_copy()
+            c.used_in_sketch = c.citation_id in used_ids
+            name = c.locator.get("decl_name") or ""
+            c.used_in_proof = bool(proof) and c.corpus == "mathlib" and (name in used_consts if used_consts is not None else bool(identifiers_used(proof, [name])))
+            citations.append(c)
+        return SolutionReport(
+            problem_id=problem.problem_id,
+            config=cfg["name"],
+            status=status,
+            attempts=final.get("attempt", 1) if status == "done" else (len(final.get("history", [])) or 1),
+            replans=final.get("replans", 0),
+            llm_calls=final.get("llm_calls", 0),
+            retrieval_calls=final.get("retrieval_calls", 0),
+            tokens_in=final.get("tokens_in", 0),
+            tokens_out=final.get("tokens_out", 0),
+            wall_seconds=round(wall, 1),
+            lean_code=final.get("lean_code", ""),
+            verdict=final.get("verdict"),
+            citations=citations,
+            n_retrieved=len(citations),
+            n_used_in_sketch=sum(c.used_in_sketch for c in citations),
+            n_used_in_proof=sum(c.used_in_proof for c in citations),
+            error_types=final.get("error_types", []) + ([final["fail_reason"]] if final.get("fail_reason") else []),
+            re_retrievals=final.get("re_retrievals", 0),
+            re_retrievals_ok=final.get("re_retrievals_ok", 0),
+            models=final.get("models", []),
+            solved_by=final.get("solved_by", "") if status == "done" else "",
+            prover_samples=final.get("prover_samples", 0),
+        )

ragsolver/orchestrator/run.py

@@ -0,0 +1,331 @@
+"""Corrida de problemas × configuraciones de ablación (propuesta §8.2) -> SolutionReport
+por (problema, config) en data/eval/runs/<run_id>/results.jsonl + resumen.
+
+Uso: python -m ragsolver.orchestrator.run --problems data/eval/problems/dev_trivial.jsonl --configs full,no_rag
+"""
+
+from __future__ import annotations
+
+import argparse
+from concurrent.futures import ThreadPoolExecutor, as_completed
+import json
+import time
+import uuid
+from pathlib import Path
+
+from ragsolver.agents.agents import Agents, InvalidLLMOutput, load_agents_config
+from ragsolver.agents.schemas import Problem, SolutionReport
+from ragsolver.lean.verify import LeanChecker, build_file, verify
+from ragsolver.llm import LLM, DailyQuotaExhausted
+from ragsolver.logging.jsonl_writer import trace_path
+from ragsolver.orchestrator.graph import Orchestrator, close_goal
+from ragsolver.prover import ProverUnavailable, local_prover
+from ragsolver.rag.embed import embed_queries
+from ragsolver.rag.retrieve import Retriever
+
+
+def load_problems(path: str | Path) -> list[Problem]:
+    return [Problem.model_validate_json(l) for l in Path(path).read_text(encoding="utf-8").splitlines() if l.strip()]
+
+
+def check_index_consistency(checker: LeanChecker, retriever: Retriever, n: int = 20, seed: int = 13) -> None:
+    """`PLAN_RAG.md §12`: `decl_name` al azar de la tabla que sirve el corpus
+    `mathlib`, comprobados con `#check` contra el Lean real del verificador — si
+    el índice tiene nombres que no existen en esta versión de Mathlib, el RAG
+    cita lemas fantasma. No aborta la corrida, sólo avisa en el log; cualquier
+    fallo (tabla ausente, REPL caído) se ignora igual."""
+    import random
+
+    try:
+        table = retriever._table("mathlib")
+        rows = table.search().select(["decl_name"]).limit(table.count_rows()).to_list()
+        names = [r["decl_name"] for r in rows if r.get("decl_name")]
+        if not names:
+            return
+        sample = random.Random(seed).sample(names, min(n, len(names)))
+        found, total = checker.check_identifiers_exist(sample)
+        print(f"[index-check] {found}/{total} decl_name de la tabla '{retriever.tables.get('mathlib', 'mathlib')}' existen en Lean", flush=True)
+        if found < total - 1:  # tolera 1 falso positivo del `#check` aproximado
+            print(f"[index-check] AVISO: {total - found} nombres del índice no se resolvieron en Lean — posibles lemas fantasma", flush=True)
+    except Exception as e:
+        print(f"[index-check] omitido: {type(e).__name__}: {e}", flush=True)
+
+
+def effective_config(base: dict, name: str) -> dict:
+    """Config efectiva de una ablación: claves del yaml + sobreescrituras de `configs[name]`."""
+    over = dict(base["configs"][name])
+    cfg = {
+        "name": name,
+        "mode": over.pop("mode", "graph"),
+        "rag": over.pop("rag", True),
+        "corpora": ["mathlib", "informal"],
+        "k_max": over.pop("k_max", base["k_max"]),
+        "max_replans": base["max_replans"],
+        "llm_budget": base["llm_budget"],
+        "retrieval": dict(base["retrieval"]),
+        "lean": dict(base["lean"]),
+        "goal_mode": over.pop("goal_mode", base.get("goal_mode", False)),
+        "close": dict(base.get("close") or {}),
+        "prover": dict(base.get("prover") or {}),
+    }
+    for k, v in over.items():  # un dict (p.ej. `prover: {k_root: 32}`) se fusiona con el de base, no lo reemplaza
+        cfg[k] = {**cfg[k], **v} if isinstance(v, dict) and isinstance(cfg.get(k), dict) else v
+    return cfg
+
+
+def drafter_agents(base: dict, trace_dir: str) -> Agents | None:
+    """Agentes con el LLM de `llm_draft` (mismo modelo, CON razonamiento) para el borrador de DRAFT; None si
+    la sección no existe en `configs/versions.yaml` (DRAFT usa entonces los agentes normales)."""
+    import yaml
+
+    if "llm_draft" not in (yaml.safe_load(open("configs/versions.yaml", encoding="utf-8")) or {}):
+        return None
+    return Agents(LLM(section="llm_draft"), base, trace_dir=trace_dir)
+
+
+def run_auto(problem: Problem, cfg: dict, checker: LeanChecker | None, agents: Agents | None = None, run_id: str = "") -> SolutionReport:
+    """Línea base `baseline_auto` (docs/PLAN_MEJORA_RAG.md Fase 6): 0 llamadas LLM, sólo la batería
+    CLOSE sin premisas sobre el goal raíz. Es lo que Lean resuelve solo; el sistema con agentes tiene
+    que superarla para justificar sus llamadas."""
+    t0 = time.time()
+    rep = SolutionReport(problem_id=problem.problem_id, config=cfg["name"], status="fail", attempts=1, error_types=["unknown"])
+    if checker is None:
+        rep.error_types = ["unsupported: baseline_auto requiere el REPL de Lean"]
+        return rep
+    lean = cfg["lean"]
+    goals, errors = checker.goals(problem.formal_statement, "sorry", problem.header, lean["max_heartbeats"])
+    block, log = (close_goal(checker, goals[0], cfg["close"]["tactics"], False, [], [], cfg["close"]["timeout_s"]) if len(goals) == 1 and not errors else (None, []))
+    if block:
+        rep.verdict = checker.check(problem.formal_statement, block, problem.header, lean["max_heartbeats"])
+        rep.lean_code = build_file(problem.formal_statement, block, lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+        if rep.verdict.ok:
+            rep.status, rep.error_types = "done", []
+    if agents is not None:
+        agents.trace("close", run_id, problem.problem_id, 1, (time.time() - t0) * 1000, {"goal": 0, "closed": bool(block), "block": (block or "")[:200], "tried": log})
+    rep.wall_seconds = round(time.time() - t0, 1)
+    return rep
+
+
+def run_prover_only(problem: Problem, cfg: dict, checker: LeanChecker | None, prover, agents: Agents | None = None, run_id: str = "") -> SolutionReport:
+    """Línea base `baseline_prover` (docs/PLAN_REDISENO_PROVER.md): 0 API, sólo el demostrador local sobre
+    el teorema completo (k_root muestras + autocorrección con los errores de Lean, SIN sugerencias del RAG)."""
+    import re as _re
+
+    from ragsolver.prover import prove
+
+    t0 = time.time()
+    rep = SolutionReport(problem_id=problem.problem_id, config=cfg["name"], status="fail", attempts=1, error_types=["unknown"])
+    if checker is None or prover is None:
+        rep.error_types = ["unsupported: baseline_prover requiere el REPL y el demostrador local"]
+        return rep
+    pcfg, lean = cfg["prover"], cfg["lean"]
+    name = _re.match(r"\s*(?:theorem|lemma)\s+(\S+)", problem.formal_statement).group(1)
+    tac, log = prove(prover, checker, problem.formal_statement, problem.header, name, k=pcfg["k_root"], correction_rounds=pcfg.get("correction_rounds", 1), retriever=None, max_heartbeats=lean["max_heartbeats"])
+    rep.prover_samples = log["samples"] + log["rounds"] * 2
+    if tac:
+        rep.verdict = checker.check(problem.formal_statement, tac, problem.header, lean["max_heartbeats"])
+        rep.lean_code = build_file(problem.formal_statement, tac, lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+        if rep.verdict.ok:
+            rep.status, rep.error_types, rep.solved_by = "done", [], "prover_root"
+    if agents is not None:
+        agents.trace("prover", run_id, problem.problem_id, 1, (time.time() - t0) * 1000, {"stage": "baseline_prover", "solved": bool(tac), **{k: v for k, v in log.items() if k not in ("suggested", "candidates")}})
+    rep.wall_seconds = round(time.time() - t0, 1)
+    return rep
+
+
+def run_baseline(mode: str, problem: Problem, cfg: dict, agents: Agents, run_id: str, checker: LeanChecker | None = None) -> SolutionReport:
+    if problem.imports:  # mismo guard que Orchestrator.solve (BUG-4): nadie usa imports adicionales por problema hoy
+        return SolutionReport(problem_id=problem.problem_id, config=cfg["name"], status="fail", error_types=[f"unsupported: Problem.imports no soportado: {problem.imports}"])
+    t0 = time.time()
+    out, resp = agents.baseline(mode, problem, run_id)
+    rep = SolutionReport(problem_id=problem.problem_id, config=cfg["name"], status="fail", attempts=1, llm_calls=1, tokens_in=resp.tokens_in, tokens_out=resp.tokens_out, models=[resp.model])
+    if mode == "baseline_a":
+        lean = cfg["lean"]
+        if checker is not None:
+            v = checker.check(problem.formal_statement, out.proof_tactics, problem.header, lean["max_heartbeats"])
+        else:
+            v = verify(problem.formal_statement, out.proof_tactics, f"{problem.problem_id}_{mode}", lean["imports"] + problem.imports, lean["timeout_s"], lean["max_heartbeats"], header=problem.header)
+        rep.verdict, rep.status = v, ("done" if v.ok else "fail")
+        # BUG-2: mismo `header` que se verificó, para que `lean_code` sea fiel.
+        rep.lean_code = build_file(problem.formal_statement, out.proof_tactics, lean["imports"] + problem.imports, lean["max_heartbeats"], header=problem.header)
+        if not v.ok:
+            rep.error_types = ["unknown"]
+    else:  # baseline_b: sin verificación formal; se reporta su autoevaluación (métrica "falsos positivos evitados")
+        rep.self_assessed_correct = out.self_assessed_correct
+        rep.status = "fail"
+    rep.wall_seconds = round(time.time() - t0, 1)
+    return rep
+
+
+def run_suite(problems: list[Problem], config_names: list[str], out_dir: str | Path, agents_yaml: str = "configs/agents.yaml", db_path: str = "data/index/lancedb", run_id: str | None = None, workers: int = 1) -> dict:
+    """Corre problemas × configs. **Reanudable**: con el mismo `run_id`, los pares
+    (config, problema) ya presentes en results.jsonl se saltan; si se agota la cuota
+    diaria de todos los modelos, corta limpio (status "quota_exhausted") para reanudar
+    al día siguiente con el mismo comando. `workers` > 1 resuelve varios pares a la vez
+    (hilos: el cuello de botella es la latencia del LLM; el REPL y las trazas van con lock)."""
+    base = load_agents_config(agents_yaml)
+    run_id = run_id or f"run-{time.strftime('%Y%m%d-%H%M')}-{uuid.uuid4().hex[:6]}"
+    out = Path(out_dir) / run_id
+    out.mkdir(parents=True, exist_ok=True)
+    results_path = out / "results.jsonl"
+    results: list[SolutionReport] = [SolutionReport.model_validate_json(l) for l in results_path.read_text(encoding="utf-8").splitlines() if l.strip()] if results_path.exists() else []
+    errors = [r for r in results if r.status == "error"]
+    if errors:  # fallo de infraestructura (excepción, red, key): se reintentan; quedan auditados en errors.jsonl
+        with (out / "errors.jsonl").open("a", encoding="utf-8") as f:
+            f.writelines(r.model_dump_json() + "\n" for r in errors)
+        results = [r for r in results if r.status != "error"]
+        results_path.write_text("".join(r.model_dump_json() + "\n" for r in results), encoding="utf-8")
+        print(f"[resume] {len(errors)} pares con status=error se reintentan (movidos a errors.jsonl)", flush=True)
+    done = {(r.config, r.problem_id) for r in results}
+    if done:
+        print(f"[resume] {len(done)} resultados previos en {results_path}", flush=True)
+
+    llm = LLM(section="llm")
+    agents = Agents(llm, base, trace_dir=str(out / "traces"))
+    retriever = Retriever(db_path=db_path)
+    retriever.trace_dir = str(out / "traces")
+    checker = LeanChecker(imports=base["lean"]["imports"], timeout_s=base["lean"]["timeout_s"]) if base["lean"].get("backend", "repl") == "repl" else None
+    prover = local_prover(base.get("prover") or {})
+    needs = [n for n in config_names if (c := effective_config(base, n))["mode"] == "baseline_prover" or any(c["prover"].get(x) for x in ("dsp", "repair", "examples"))]
+    if needs and prover is None:  # sin demostrador estas configuraciones degradarían en silencio (fallos falsos o el bucle por API)
+        raise SystemExit(f"[prover] {needs} necesitan el demostrador local y no responde: `bash scripts/prover_server.sh start`")
+    drafter = drafter_agents(base, str(out / "traces"))
+    orchestrator = Orchestrator(agents, retriever, checker, prover, drafter)
+    if checker is not None:  # arranca el REPL (`import Mathlib`, minutos) fuera del reloj de los problemas
+        checker.check("theorem _warmup : True := by sorry", "trivial")
+    if getattr(retriever, "versions", None):  # carga el embedder antes de los hilos (los fakes de los tests no lo tienen)
+        embed_queries(["warmup"], model_name=retriever.versions["embedding"]["model"])
+    if checker is not None and getattr(retriever, "versions", None):
+        check_index_consistency(checker, retriever)
+
+    def solve_pair(name: str, problem: Problem) -> SolutionReport:
+        cfg = effective_config(base, name)
+        pid = f"{run_id}:{name}:{problem.problem_id}"
+        tp = trace_path(pid, out / "traces")
+        if tp.exists():  # intento anterior interrumpido (sin fila en results.jsonl): se aparta para no mezclar eventos
+            (out / "traces" / "interrupted").mkdir(exist_ok=True)
+            tp.rename(out / "traces" / "interrupted" / f"{tp.stem}.{int(time.time())}.jsonl")
+        if cfg["mode"] == "baseline_auto":
+            return run_auto(problem, cfg, checker, agents, pid)
+        if cfg["mode"] == "baseline_prover":
+            return run_prover_only(problem, cfg, checker, prover, agents, pid)
+        if cfg["mode"].startswith("baseline"):
+            try:
+                return run_baseline(cfg["mode"], problem, cfg, agents, pid, checker)
+            except DailyQuotaExhausted:
+                raise
+            except Exception as e:  # una línea base que explota no puede tumbar la corrida entera
+                # ACC-1: si es InvalidLLMOutput, .model existe (el modelo que produjo la salida rota);
+                # antes esta fila quedaba con `models=[]`, sin poder saber qué modelo falló.
+                models = [e.model] if isinstance(e, InvalidLLMOutput) and getattr(e, "model", None) else []
+                return SolutionReport(problem_id=problem.problem_id, config=cfg["name"], status="fail" if isinstance(e, InvalidLLMOutput) else "error", attempts=1, llm_calls=getattr(e, "calls", 0), tokens_in=getattr(e, "tokens_in", 0), tokens_out=getattr(e, "tokens_out", 0), models=models, error_types=[f"llm_output_invalid:{e.agent}" if isinstance(e, InvalidLLMOutput) else f"exception: {type(e).__name__}: {str(e)[:300]}"])
+        return orchestrator.solve(problem, cfg, pid)
+
+    pairs = [(n, p) for n in config_names for p in problems if (n, p.problem_id) not in done]
+    status = "completed"
+    with results_path.open("a", encoding="utf-8") as f, ThreadPoolExecutor(max_workers=workers) as pool:
+        futures = {pool.submit(solve_pair, n, p): (n, p) for n, p in pairs}
+        try:
+            for fut in as_completed(futures):
+                name, problem = futures[fut]
+                rep = fut.result()
+                results.append(rep)
+                f.write(rep.model_dump_json() + "\n")
+                f.flush()
+                print(f"[{name}] {problem.problem_id}: {rep.status} attempts={rep.attempts} llm_calls={rep.llm_calls} used_in_proof={rep.n_used_in_proof}/{rep.n_retrieved} {rep.wall_seconds}s", flush=True)
+        except DailyQuotaExhausted as e:
+            status = "quota_exhausted"
+            print(f"[stop] cuota diaria agotada en todos los modelos ({e}); reanudar mañana con --run-id {run_id}", flush=True)
+            for fu in futures:
+                fu.cancel()
+        except ProverUnavailable as e:
+            status = "prover_down"
+            print(f"[stop] el demostrador local dejó de responder ({e}); `bash scripts/prover_server.sh start` y reanudar con --run-id {run_id}", flush=True)
+            for fu in futures:
+                fu.cancel()
+    if checker is not None:
+        checker.close()
+    llms = [llm] + ([drafter.llm] if drafter is not None else [])
+    calls, cost = sum(x.calls for x in llms), sum(getattr(x, "cost_usd", 0.0) for x in llms)
+    print(f"[cost] {calls} llamadas, {sum(x.tokens_in for x in llms)} tokens de entrada, {sum(x.tokens_out for x in llms)} de salida, US${cost:.4f} (OpenRouter usage.cost)", flush=True)
+    summary = summarize(results)
+    (out / "summary.json").write_text(json.dumps(summary, indent=2, ensure_ascii=False), encoding="utf-8")
+    pending = [(n, p.problem_id) for n in config_names for p in problems if (n, p.problem_id) not in {(r.config, r.problem_id) for r in results}]
+    return {"run_id": run_id, "out": str(out), "status": status, "n_done": len(results), "n_pending": len(pending), "summary": summary, "llm_calls_total": calls, "cost_usd_total": round(cost, 4), "models_exhausted": llm.exhausted}
+
+
+def summarize(results: list[SolutionReport]) -> dict:
+    by_cfg: dict[str, list[SolutionReport]] = {}
+    for r in results:
+        by_cfg.setdefault(r.config, []).append(r)
+    summary = {}
+    for name, rs in by_cfg.items():
+        n = len(rs)
+        solved = sum(r.status == "done" for r in rs)
+        retrieved = sum(r.n_retrieved for r in rs)
+        summary[name] = {
+            "n": n,
+            "pass@1": round(solved / n, 3) if n else None,
+            "pass@1_wilson95": wilson(solved, n),
+            "llm_calls_mean": round(sum(r.llm_calls for r in rs) / n, 2) if n else None,
+            "tokens_mean": round(sum(r.tokens_in + r.tokens_out for r in rs) / n) if n else None,
+            "wall_s_median": sorted(r.wall_seconds for r in rs)[n // 2] if n else None,
+            "retrieval_calls_mean": round(sum(r.retrieval_calls for r in rs) / n, 2) if n else None,
+            "llm_calls_mean_ci95_bootstrap": bootstrap_mean_ci([r.llm_calls for r in rs]),
+            "tokens_mean_ci95_bootstrap": bootstrap_mean_ci([r.tokens_in + r.tokens_out for r in rs]),
+            "wall_s_mean_ci95_bootstrap": bootstrap_mean_ci([r.wall_seconds for r in rs]),
+            "pass_by_attempt": pass_by_attempt(rs),  # §8.3 robustez del refinamiento: acumulado por intento
+            "lemma_use_precision": round(sum(r.n_used_in_proof for r in rs) / retrieved, 3) if retrieved else None,
+            "re_retrieval_success": round(sum(r.re_retrievals_ok for r in rs) / sum(r.re_retrievals for r in rs), 3) if sum(r.re_retrievals for r in rs) else None,
+            "error_taxonomy": _count_errors(rs),
+            "self_assessed_correct": sum(1 for r in rs if r.self_assessed_correct) if any(r.self_assessed_correct is not None for r in rs) else None,
+        }
+    return summary
+
+
+def _count_errors(rs: list[SolutionReport]) -> dict:
+    counts: dict[str, int] = {}
+    for r in rs:
+        for e in r.error_types:
+            counts[e] = counts.get(e, 0) + 1
+    return counts
+
+
+def pass_by_attempt(rs: list[SolutionReport]) -> dict[str, float]:
+    """Fracción resuelta con ≤ i intentos (la ganancia marginal es la diferencia entre columnas)."""
+    n = len(rs)
+    k_max = max((r.attempts for r in rs), default=1)
+    return {str(i): round(sum(1 for r in rs if r.status == "done" and r.attempts <= i) / n, 3) for i in range(1, k_max + 1)} if n else {}
+
+
+def bootstrap_mean_ci(xs: list[float], n_boot: int = 1000, seed: int = 13) -> list[float] | None:
+    """IC 95 % bootstrap de la media (propuesta §8.4: costo y latencia)."""
+    import random
+
+    if not xs:
+        return None
+    rng = random.Random(seed)
+    means = sorted(sum(rng.choice(xs) for _ in xs) / len(xs) for _ in range(n_boot))
+    return [round(means[int(0.025 * n_boot)], 2), round(means[int(0.975 * n_boot) - 1], 2)]
+
+
+def wilson(k: int, n: int, z: float = 1.96) -> list[float] | None:
+    if not n:
+        return None
+    p = k / n
+    d = 1 + z * z / n
+    c = (p + z * z / (2 * n)) / d
+    h = z * ((p * (1 - p) / n + z * z / (4 * n * n)) ** 0.5) / d
+    return [round(max(0.0, c - h), 3), round(min(1.0, c + h), 3)]
+
+
+if __name__ == "__main__":
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--problems", required=True)
+    ap.add_argument("--configs", default="full")
+    ap.add_argument("--out", default="data/eval/runs")
+    ap.add_argument("--run-id", default=None)
+    ap.add_argument("--workers", type=int, default=1)
+    args = ap.parse_args()
+    res = run_suite(load_problems(args.problems), args.configs.split(","), args.out, run_id=args.run_id, workers=args.workers)
+    print(json.dumps(res, indent=2, ensure_ascii=False))

ragsolver/prover.py

@@ -0,0 +1,302 @@
+"""Demostrador especializado en Lean servido en la GPU local (docs/PLAN_REDISENO_PROVER.md).
+
+Goedel-Prover-V2-8B (Apache-2.0; 84.6 % pass@32 en miniF2F según su paper) vía `llama-server`
+(OpenAI-compatible, Vulkan). Genera k pruebas en paralelo; de cada una se toma SÓLO el bloque de
+tácticas del teorema pedido y se empalma en el enunciado del problema (el modelo nunca puede debilitar
+el enunciado); cada candidato pasa por `LeanChecker.check` (validador + kernel + axiomas).
+
+Autocorrección: el modelo se entrenó con Lean 4.9 y su Mathlib; el verificador usa v4.28, así que usa
+nombres renombrados o borrados. Ante `unknown identifier/constant`, el RAG busca declaraciones parecidas
+QUE EXISTEN en el entorno (índice + `#check`) y se las da al modelo junto con los errores de Lean.
+Costo de API: 0 (todo local).
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+import os
+import re
+import textwrap
+import threading
+import time
+from concurrent.futures import ThreadPoolExecutor
+from pathlib import Path
+
+import httpx
+
+PROMPT = """Complete the following Lean 4 code:
+
+```lean4
+{}```
+
+Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
+The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof."""
+
+_FENCE_RE = re.compile(r"```(?:lean4|lean)?[ \t]*\n(.*?)```", re.S)
+_UNKNOWN_RE = re.compile(r"[Uu]nknown (?:identifier|constant) [`']([^`']+)[`']")
+
+
+def prover_url() -> str:
+    """`RAGSOLVER_PROVER_URL` o el `llama-server` de Windows en el gateway de WSL, puerto 8082."""
+    if os.environ.get("RAGSOLVER_PROVER_URL"):
+        return os.environ["RAGSOLVER_PROVER_URL"].rstrip("/")
+    gw = "127.0.0.1"
+    try:
+        for line in open("/proc/net/route"):
+            f = line.split()
+            if f[1] == "00000000":
+                gw = ".".join(str(int(f[2][i : i + 2], 16)) for i in (6, 4, 2, 0))
+                break
+    except OSError:
+        pass
+    return f"http://{gw}:8082"
+
+
+def lean_input(formal_statement: str, header: str) -> str:
+    """El archivo que espera el modelo: imports, opens y el teorema con `sorry`."""
+    stmt = re.sub(r":=\s*by\s+sorry\s*$|:=\s*sorry\s*$", "", formal_statement.rstrip()).rstrip()
+    opens = "\n".join(l for l in header.splitlines() if l.strip() and not l.strip().startswith("import"))
+    return f"import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 400000\n\n{opens}\n\n{stmt} := by\n  sorry"
+
+
+def extract_tactics(output: str, theorem_name: str) -> str | None:
+    """Tácticas del teorema `theorem_name` en el último bloque de código de la salida, o None.
+    Se descarta todo lo demás (enunciado, lemas auxiliares, comandos): el enunciado lo pone el problema."""
+    for block in reversed(_FENCE_RE.findall(output)):
+        m = re.search(rf"(?:theorem|lemma)\s+{re.escape(theorem_name)}\b.*?:=\s*by[ \t]*\n(.*)", block, re.S)
+        if not m:
+            continue
+        lines = m.group(1).splitlines()
+        body = []
+        for line in lines:  # el cuerpo termina en la primera línea sin sangría (otra declaración, comando)
+            if line.strip() and not line[0].isspace():
+                break
+            body.append(line)
+        tactics = "\n".join(body).strip("\n")
+        if tactics.strip():
+            from textwrap import dedent
+
+            return dedent(tactics)
+    return None
+
+
+def unknown_names(errors: list[dict]) -> list[str]:
+    return list(dict.fromkeys(n for e in errors for n in _UNKNOWN_RE.findall(e.get("message", ""))))
+
+
+class ProverUnavailable(RuntimeError):
+    """El servidor del demostrador dejó de responder: el runner corta la corrida (como con la cuota diaria)."""
+
+
+def local_prover(pcfg: dict) -> LocalProver | None:
+    """El demostrador si `prover.enabled` y el servidor responde; si no, None (el sistema sigue sin él)."""
+    if not pcfg.get("enabled"):
+        return None
+    p = LocalProver(max_tokens=pcfg.get("max_tokens", 12000), temperature=pcfg.get("temperature", 0.8))
+    if p.alive():
+        print(f"[prover] demostrador local en {p.url}", flush=True)
+        return p
+    print(f"[prover] AVISO: {p.url} no responde; se corre sin demostrador local", flush=True)
+    return None
+
+
+class LocalProver:
+    def __init__(self, url: str | None = None, max_tokens: int = 12000, temperature: float = 0.8, timeout_s: float = 1800, cache_path: str | None = "data/eval/prover_cache.jsonl"):
+        self.url = url or prover_url()
+        self.max_tokens, self.temperature, self.timeout_s = max_tokens, temperature, timeout_s
+        self.client = httpx.Client(timeout=timeout_s)
+        self.tokens_out = 0
+        self.calls = 0
+        # caché en disco por (mensajes, semilla, parámetros): dos configuraciones que piden la misma muestra
+        # (p.ej. `baseline_prover` y la etapa 0 de `full`) la generan una sola vez, y quedan pareadas
+        self.cache_path = Path(cache_path) if cache_path else None
+        self._cache: dict[str, str] = {}
+        self._lock = threading.Lock()
+        if self.cache_path and self.cache_path.exists():
+            for line in self.cache_path.open(encoding="utf-8"):
+                if line.strip():
+                    d = json.loads(line)
+                    self._cache[d["key"]] = d["out"]
+
+    def alive(self) -> bool:
+        try:
+            return self.client.get(f"{self.url}/health", timeout=5).status_code == 200
+        except httpx.HTTPError:
+            return False
+
+    def _chat(self, messages: list[dict], seed: int) -> str:
+        key = hashlib.sha256(json.dumps([messages, seed, self.max_tokens, self.temperature], ensure_ascii=False).encode()).hexdigest()
+        if key in self._cache:
+            return self._cache[key]
+        r = self.client.post(f"{self.url}/v1/chat/completions", json={"messages": messages, "max_tokens": self.max_tokens, "temperature": self.temperature, "top_p": 0.95, "seed": seed})
+        r.raise_for_status()
+        d = r.json()
+        self.calls += 1
+        self.tokens_out += (d.get("usage") or {}).get("completion_tokens", 0)
+        msg = d["choices"][0]["message"]
+        # el razonamiento (si el servidor lo separa) va ANTES: la extracción toma el último bloque de código
+        out = ((msg.get("reasoning_content") or "") + "\n" + (msg.get("content") or "")).strip()
+        with self._lock:
+            self._cache[key] = out
+            if self.cache_path:
+                with self.cache_path.open("a", encoding="utf-8") as f:
+                    f.write(json.dumps({"key": key, "out": out}, ensure_ascii=False) + "\n")
+        return out
+
+    def sample(self, messages: list[dict], k: int, seed0: int = 13) -> list[str]:
+        with ThreadPoolExecutor(max_workers=k) as pool:
+            outs = list(pool.map(lambda i: self._safe_chat(messages, seed0 + i), range(k)))
+        # una muestra que falla se tolera; todas fallando con el servidor caído no son "muestras sin prueba":
+        # la corrida se detiene y se reanuda (eval-v4: el servidor murió y 22 problemas quedaron como fallos falsos)
+        if outs and all(o.startswith("(prover error") for o in outs) and not self.alive():
+            raise ProverUnavailable(f"{self.url} no responde")
+        return outs
+
+    def _safe_chat(self, messages: list[dict], seed: int) -> str:
+        try:
+            return self._chat(messages, seed)
+        except httpx.HTTPError as e:
+            return f"(prover error: {type(e).__name__})"
+
+
+def name_suggestions(names: list[str], checker, retriever=None, header: str = "", k: int = 4) -> tuple[str, dict[str, str]]:
+    """RAG para la autocorrección: por cada nombre desconocido, declaraciones parecidas que SÍ existen en
+    el entorno de Lean del verificador (búsqueda en el índice por los tokens del nombre + `#check`)."""
+    lines, suggested = [], {}
+    for n in names[:4]:
+        cands: list[str] = []
+        if retriever is not None:
+            from ragsolver.rag.schema import RetrievalRequest
+
+            try:
+                res = retriever.search(RetrievalRequest(queries=[f"unknown identifier '{n}'"], mode="error", corpora=["mathlib"], k=k * 2, n_candidates=50, rerank=False, include_figures=False, context={"problem_id": "", "agent": "prover"}))
+                cands = [h.metadata.get("decl_name") for h in res.hits if h.metadata.get("decl_name")]
+            except Exception:
+                cands = []
+        sigs = checker.signatures(cands[: k * 2], header=header) if cands else {}
+        suggested.update(list(sigs.items())[:k])
+        if sigs:
+            lines.append(f"`{n}` does not exist in this Mathlib version. Existing declarations with similar names:\n" + "\n".join(f"  {c} : {t[:200]}" for c, t in list(sigs.items())[:k]))
+        else:
+            lines.append(f"`{n}` does not exist in this Mathlib version.")
+    return "\n".join(lines), suggested
+
+
+def draft_hint(strategy: str, steps: list[str], sketch: str, lemmas: dict[str, str], max_sketch: int = 4000) -> str:
+    """Draft-Sketch-Prove: el plan y la prueba informal del modelo de la API, más los lemas que recuperó el
+    RAG (que existen en el Mathlib fijado), como guía dentro del prompt del demostrador."""
+    parts = ["Here is an informal proof written by another model. It may contain mistakes: use it as guidance, not as ground truth.", f"Strategy: {strategy}"]
+    parts += [f"{i}. {s}" for i, s in enumerate(steps, 1)]
+    parts.append(f"Informal proof:\n{sketch[:max_sketch]}")
+    if lemmas:
+        parts.append("Mathlib lemmas that may be useful (they exist in the installed Mathlib version):\n" + "\n".join(f"  {n} : {t[:200]}" for n, t in lemmas.items()))
+    return "\n\n".join(parts)
+
+
+def examples_hint(hits: list[dict], max_proof: int = 1500) -> str:
+    """RAG de pruebas (`rag/proofs.py`): pruebas verificadas de problemas parecidos como ejemplos en el prompt."""
+    blocks = [f"```lean4\n{h['statement']} := by\n{textwrap.indent(h['proof'][:max_proof], '  ')}\n```" for h in hits]
+    return "Verified Lean 4 proofs of similar problems (older Mathlib: some names may have changed). Reuse their techniques and hints where they fit:\n\n" + "\n\n".join(blocks)
+
+
+def prove(prover: LocalProver, checker, formal_statement: str, header: str, theorem_name: str, k: int = 4, correction_rounds: int = 1, retriever=None, max_heartbeats: int = 400000, batch: int = 4, hint: str = "") -> tuple[str | None, dict]:
+    """k muestras en lotes de `batch` en paralelo, con salida temprana: la primera que pasa `check` gana
+    (los problemas fáciles no pagan las k). Si ninguna, una ronda de autocorrección sobre las (hasta) 2
+    muestras con tácticas extraíbles: errores de Lean + sugerencias de nombres (RAG, si `retriever`).
+    `hint` (Draft-Sketch-Prove, `draft_hint`) se agrega al prompt; el prompt cambia, así que sus muestras
+    no comparten caché con las de la etapa 0."""
+    t0 = time.time()
+    user = PROMPT.format(lean_input(formal_statement, header)) + (f"\n\n{hint}" if hint else "")
+    log = {"samples": 0, "extracted": 0, "rounds": 0, "corrections_with_rag": 0, "suggested": {}}
+    pending, failed = [], []  # failed: todo candidato extraíble que Lean rechazó, para REPAIR (graph.py)
+    for start in range(0, k, batch):
+        outs = prover.sample([{"role": "user", "content": user}], min(batch, k - start), seed0=13 + start)
+        log["samples"] += len(outs)  # generadas (trabajo de GPU), no sólo las revisadas antes del éxito
+        for out in outs:
+            tac = extract_tactics(out, theorem_name)
+            if not tac:
+                continue
+            log["extracted"] += 1
+            v = checker.check(formal_statement, tac, header, max_heartbeats)
+            if v.ok:
+                log["seconds"] = round(time.time() - t0, 1)
+                return tac, {**log, "solved_in": "sample"}
+            pending.append((out, tac, v))
+            failed.append((tac, v))
+    for rnd in range(correction_rounds):
+        if not pending:
+            break
+        log["rounds"] += 1
+        nxt = []
+        for out, tac, v in pending[:2]:
+            err = "\n".join(f"line {e['line']}: {e['message'][:400]}" for e in v.errors[:6])
+            names = unknown_names(v.errors)
+            hint, sugg = name_suggestions(names, checker, retriever, header) if names else ("", {})
+            log["suggested"].update(sugg)
+            log["corrections_with_rag"] += bool(sugg)
+            fix = f"The proof failed to compile in Lean 4 (recent Mathlib). Errors:\n{err}\n" + (f"\n{hint}\n" if hint else "") + "\nFix the proof and output the complete corrected Lean 4 code."
+            answer = out.rsplit("</think>", 1)[-1][-6000:]  # la respuesta final, sin el razonamiento
+            outs2 = prover.sample([{"role": "user", "content": user}, {"role": "assistant", "content": answer}, {"role": "user", "content": fix}], 1, seed0=100 + rnd)
+            tac2 = extract_tactics(outs2[0], theorem_name)
+            if not tac2:
+                continue
+            v2 = checker.check(formal_statement, tac2, header, max_heartbeats)
+            if v2.ok:
+                log["seconds"] = round(time.time() - t0, 1)
+                return tac2, {**log, "solved_in": f"correction{rnd + 1}"}
+            nxt.append((outs2[0], tac2, v2))
+            failed.append((tac2, v2))
+        pending = nxt
+    log["seconds"] = round(time.time() - t0, 1)
+    # casi-pruebas para REPAIR, menos errores primero: Lean sigue elaborando tras un `have` que falla, así que
+    # ≤ 2 errores ≈ ≤ 2 pasos malos; con más, reparar paso a paso cuesta horas de GPU (smoke 2026-10-21)
+    log["candidates"] = [t for t, v in sorted(failed, key=lambda x: len(x[1].errors)) if len(v.errors) <= 2]
+    return None, log
+
+
+_DAGGER_RE = re.compile(r"([A-Za-z_][\w']*)✝(\d*)")
+
+
+def goal_to_theorem(goal: str, name: str) -> str | None:
+    """Un goal pretty-printed del REPL ("a b : ℝ\\nh : 0 < a\\n⊢ T") como teorema autónomo, para pedírselo
+    al demostrador (receta de DeepSeek-Prover-V2: cada subobjetivo como lema). Los nombres inaccesibles
+    (`x✝`) se renombran; las instancias (`inst✝ : Fact p`) pasan a `[Fact p]`. None si no se puede."""
+    lines = [l for l in goal.splitlines() if l.strip() and not l.startswith("case ")]
+    if not lines or "⊢" not in goal:
+        return None
+    hyps, target = [], None
+    for i, l in enumerate(lines):
+        if l.startswith("⊢"):
+            target = " ".join([l[1:].strip()] + [x.strip() for x in lines[i + 1 :]])
+            break
+        if l[0].isspace() and hyps:  # continuación de la hipótesis anterior
+            hyps[-1] += " " + l.strip()
+        else:
+            hyps.append(l.strip())
+    if target is None:
+        return None
+    binders = []
+    for h in hyps:
+        if " : " not in h:
+            return None
+        names, typ = h.split(" : ", 1)
+        if all(n.startswith("inst✝") for n in names.split()):
+            binders.append(f"[{typ}]")
+        else:
+            binders.append(f"({names} : {typ})")
+    stmt = f"theorem {name} " + " ".join(binders) + f" : {target} := by sorry"
+    return _DAGGER_RE.sub(lambda m: f"{m.group(1)}_{m.group(2) or 0}", stmt)
+
+
+def renamed_inaccessible(goal: str) -> list[str]:
+    """Nombres que `goal_to_theorem` dio a las hipótesis inaccesibles (no instancias), en orden: un
+    bloque probado para el lema autónomo funciona en el contexto original con `rename_i <estos>` delante."""
+    names = []
+    for l in goal.split("⊢", 1)[0].splitlines():
+        if " : " in l and not l[0].isspace():
+            for n in l.split(" : ", 1)[0].split():
+                m = _DAGGER_RE.fullmatch(n)
+                if m and not n.startswith("inst✝"):
+                    names.append(f"{m.group(1)}_{m.group(2) or 0}")
+    return names

ragsolver/rag/embed.py

@@ -0,0 +1,128 @@
+"""Wrapper de embeddings (Qwen3-Embedding) usado por ambos corpus.
+
+docs/PLAN_RAG.md §9.1: un solo modelo para Mathlib e informal. Documentos se
+embeben sin instrucción; las consultas llevan instrucción (recomendación del
+model card de Qwen3-Embedding — mejora retrieval sin tocar el índice).
+
+Backends (`RAGSOLVER_EMBED_BACKEND`):
+- `torch` (default): sentence-transformers en CPU (bf16), ~5 textos/s.
+- `llama`: `llama-server` (llama.cpp, Vulkan) corriendo del lado de Windows con el
+  GGUF f16 del mismo modelo — usa la RX 9060 XT esquivando el bug de ROCm en WSL2
+  (docs/DECISIONS.md #48): ~48 textos/s, vectores idénticos (cos ≥ 0.9998).
+  URL en `RAGSOLVER_EMBED_URL` (default: gateway de WSL, puerto 8081).
+"""
+
+from __future__ import annotations
+
+import os
+import threading
+from functools import lru_cache
+
+# Un solo hilo carga y usa el modelo de torch: cargas concurrentes (lru_cache no lo impide) duplican
+# la RAM y dejan el modelo a medio convertir a bf16 ("expected m1 and m2 to have the same dtype")
+_TORCH_LOCK = threading.Lock()
+
+QUERY_INSTRUCTION = "Instruct: Given a mathematical query, retrieve relevant Mathlib declarations or worked problems.\nQuery: "
+
+
+@lru_cache(maxsize=1)
+def _get_model(model_name: str):
+    # Import perezoso: torch/sentence-transformers son pesados y no hacen falta
+    # para el resto del módulo (ingesta, esquema, índice sin embeddings).
+    import torch
+    from sentence_transformers import SentenceTransformer
+
+    device = "cuda" if torch.cuda.is_available() else "cpu"
+    # ponytail: sin flash_attention_2 (CUDA-only, no compila en ROCm —
+    # docs/PLAN_RAG.md §9.4); se usa la implementación de atención por defecto.
+    # bfloat16 en CPU: mitad de RAM (1.2 GB vs 2.4 GB para 0.6B); la máquina tiene 7.5 GB
+    # y el pipeline de Fase 4 convive con el REPL de Lean (docs/DECISIONS.md #40).
+    dtype = torch.bfloat16 if os.environ.get("RAGSOLVER_EMBED_BF16", "1") == "1" else torch.float32
+    return SentenceTransformer(model_name, device=device, model_kwargs={"torch_dtype": dtype})
+
+
+def _backend() -> str:
+    return os.environ.get("RAGSOLVER_EMBED_BACKEND", "torch")
+
+
+def _llama_url() -> str:
+    url = os.environ.get("RAGSOLVER_EMBED_URL")
+    if url:
+        return url
+    import subprocess
+
+    gw = subprocess.run(["sh", "-c", "ip route show default | awk '{print $3}'"], capture_output=True, text=True).stdout.strip() or "127.0.0.1"
+    return f"http://{gw}:8081/v1/embeddings"
+
+
+def _llama_embed(texts: list[str], batch_size: int = 64, workers: int = 8) -> list[list[float]]:
+    """Lotes concurrentes contra llama-server (8 slots). Textos truncados a 6000 caracteres
+    (ventana por slot de 2048 tokens); el servidor normaliza L2."""
+    from concurrent.futures import ThreadPoolExecutor
+
+    import httpx
+
+    url = _llama_url()
+    client = httpx.Client(timeout=900)
+    batches = [[t[:6000] for t in texts[i : i + batch_size]] for i in range(0, len(texts), batch_size)]
+
+    def one(batch):
+        for attempt in range(5):
+            try:
+                r = client.post(url, json={"input": batch})
+                r.raise_for_status()
+                data = sorted(r.json()["data"], key=lambda d: d["index"])
+                return [d["embedding"] for d in data]
+            except Exception:
+                if attempt == 4:
+                    raise
+        return []
+
+    with ThreadPoolExecutor(workers) as ex:
+        out = []
+        for vecs in ex.map(one, batches):
+            out.extend(vecs)
+    return out
+
+
+def embed_documents(texts: list[str], model_name: str, batch_size: int = 32) -> list[list[float]]:
+    """Embebe texto de documento (sin instrucción). Usado en la ingesta (offline)."""
+    if _backend() == "llama":
+        return _llama_embed(texts)
+    with _TORCH_LOCK:
+        model = _get_model(model_name)
+        vectors = model.encode(texts, batch_size=batch_size, show_progress_bar=False, normalize_embeddings=True)
+    return vectors.tolist()
+
+
+def embed_queries(texts: list[str], model_name: str, batch_size: int = 8, instruction: str | None = None) -> list[list[float]]:
+    """Embebe texto de consulta (con instrucción). Usado por el retriever (online).
+
+    `instruction`: texto tras "Instruct:" (configs/retrieval.yaml `query_instructions`);
+    por defecto la instrucción con la que se midió la Fase 1.
+    """
+    prefix = f"Instruct: {instruction}\nQuery: " if instruction else QUERY_INSTRUCTION
+    with _QUERY_CACHE_LOCK:
+        found = {t: _QUERY_CACHE.get((prefix, t, model_name)) for t in texts}
+    missing = [t for t, v in found.items() if v is None]
+    if missing:
+        if _backend() == "llama":
+            vectors_list = _llama_embed([prefix + t for t in missing])
+        else:
+            with _TORCH_LOCK:
+                model = _get_model(model_name)
+                vectors_list = model.encode([prefix + t for t in missing], batch_size=batch_size, show_progress_bar=False, normalize_embeddings=True).tolist()
+        with _QUERY_CACHE_LOCK:  # BUG-6: dict mutado desde varios hilos (--workers) sin lock podía romper la evicción a mitad de iteración
+            for t, v in zip(missing, vectors_list):
+                found[t] = v
+                _QUERY_CACHE[(prefix, t, model_name)] = v
+            while len(_QUERY_CACHE) > _QUERY_CACHE_MAX:  # ponytail: LRU aproximado (FIFO)
+                _QUERY_CACHE.pop(next(iter(_QUERY_CACHE)), None)
+    return [found[t] for t in texts]
+
+
+# Caché de embeddings de consulta (docs/PLAN_RAG.md Fase 3, tarea 1): el orquestador
+# repite consultas entre intentos (mismo subobjetivo, re-recuperación tras error).
+_QUERY_CACHE: dict[tuple[str, str, str], list[float]] = {}
+_QUERY_CACHE_MAX = 512
+_QUERY_CACHE_LOCK = threading.Lock()

ragsolver/rag/embed_corpus.py

@@ -0,0 +1,74 @@
+"""Embebe un corpus normalizado (data/corpus/*.jsonl) in-place: agrega
+`embedding`, `embedding_model`, `embedding_dim`, `index_version` a cada línea.
+
+Genérico para ambos corpus (mathlib/informal) — sólo depende de que cada línea
+tenga un campo `text` (docs/PLAN_RAG.md §9.1: un solo modelo para ambos).
+
+Uso: python -m ragsolver.rag.embed_corpus --in data/corpus/mathlib.jsonl --out data/corpus/mathlib_embedded.jsonl
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import time
+from pathlib import Path
+
+import yaml
+
+from ragsolver.rag.embed import embed_documents
+
+
+def run(in_path: str, out_path: str, versions_path: str = "configs/versions.yaml", batch_size: int = 32, chunk: int = 2048) -> dict:
+    """Streaming: lee/embebe/escribe por bloques de `chunk` filas (278k filas × 1024 floats no caben en RAM)."""
+    with open(versions_path, encoding="utf-8") as f:
+        versions = yaml.safe_load(f)
+    model_name = versions["embedding"]["model"]
+    index_version = versions["index"]["version"]
+
+    out = Path(out_path)
+    out.parent.mkdir(parents=True, exist_ok=True)
+    n, dim, t0 = 0, 0, time.time()
+    with open(in_path, encoding="utf-8") as fin, out.open("w", encoding="utf-8") as fout:
+        rows: list[dict] = []
+
+        def flush():
+            nonlocal n, dim
+            if not rows:
+                return
+            vectors = embed_documents([r["text"] for r in rows], model_name=model_name, batch_size=batch_size)
+            for row, vec in zip(rows, vectors):
+                row["embedding"] = vec
+                row["embedding_model"] = model_name
+                row["embedding_dim"] = len(vec)
+                row["index_version"] = index_version
+                fout.write(json.dumps(row, ensure_ascii=False) + "\n")
+            n += len(rows)
+            dim = len(vectors[0]) if vectors else dim
+            rows.clear()
+            print(f"  {n} textos, {n / (time.time() - t0):.1f}/s", flush=True)
+
+        for line in fin:
+            if line.strip():
+                rows.append(json.loads(line))
+            if len(rows) >= chunk:
+                flush()
+        flush()
+    dt = time.time() - t0
+    return {"n": n, "seconds": round(dt, 1), "texts_per_sec": round(n / dt, 2) if dt > 0 else None, "model": model_name, "dim": dim, "backend": __import__("os").environ.get("RAGSOLVER_EMBED_BACKEND", "torch"), "out": str(out)}
+
+
+if __name__ == "__main__":
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--in", dest="in_path", required=True)
+    ap.add_argument("--out", dest="out_path", required=True)
+    ap.add_argument("--versions", default="configs/versions.yaml")
+    ap.add_argument("--batch-size", type=int, default=32)
+    ap.add_argument("--backend", default=None, choices=["torch", "llama"], help="por defecto RAGSOLVER_EMBED_BACKEND o torch")
+    args = ap.parse_args()
+    if args.backend:
+        import os
+
+        os.environ["RAGSOLVER_EMBED_BACKEND"] = args.backend
+    stats = run(args.in_path, args.out_path, args.versions, args.batch_size)
+    print(json.dumps(stats, indent=2))

ragsolver/rag/enrich.py

@@ -0,0 +1,261 @@
+"""Fase 2, tarea 6 — enriquecimiento offline con el VLM/LLM (docs/PLAN_RAG.md §6.2).
+
+Proveedor: el que diga configs/versions.yaml `vlm_enrichment` (ragsolver.llm.LLM:
+Gemini u OpenAI-compatible). Todas las llamadas son offline (indexación); el
+retriever sigue en 0 llamadas (RNF-3).
+
+Operaciones (prompts versionados en configs/ingest.yaml `enrich:`):
+- transcribe_region: Plan B acotado — transcribe una región que MinerU se saltó.
+- describe_figure  (6a): recorte + enunciado -> descripción estructurada.
+- qa_formulas      (6b): imagen de página + LaTeX extraído -> LaTeX corregido.
+- summarize_card   (6c): problem card -> context_summary, math_area, techniques, ...
+- split_solution: casos ambiguos del emparejamiento (numeral perdido por el OCR).
+
+Caché JSONL por operación (data/parsed/<doc_id>/enrich/<op>.jsonl) con clave =
+sha256(prompt_version + entradas): re-ejecutar la ingesta no repite llamadas.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+import re
+import threading
+from concurrent.futures import ThreadPoolExecutor
+from difflib import SequenceMatcher
+from pathlib import Path
+
+import yaml
+
+from ragsolver.llm import LLM, DailyQuotaExhausted  # noqa: F401  (re-export para tests/llamadores)
+
+_FIGURE_SCHEMA = {
+    "type": "object",
+    "properties": {
+        "description": {"type": "string"},
+        "labels": {"type": "array", "items": {"type": "string"}},
+        "objects": {"type": "array", "items": {"type": "string"}},
+        "relations": {"type": "array", "items": {"type": "string"}},
+        "given_values": {"type": "array", "items": {"type": "string"}},
+        "figure_type": {"type": "string", "enum": ["geometric_diagram", "grid", "plot", "table_image", "other"]},
+    },
+    "required": ["description", "labels", "objects", "relations", "given_values", "figure_type"],
+}
+_FORMULAS_SCHEMA = {
+    "type": "object",
+    "properties": {
+        "items": {
+            "type": "array",
+            "items": {
+                "type": "object",
+                "properties": {"i": {"type": "integer"}, "latex": {"type": "string"}, "changed": {"type": "boolean"}},
+                "required": ["i", "latex", "changed"],
+            },
+        }
+    },
+    "required": ["items"],
+}
+_CARD_SCHEMA = {
+    "type": "object",
+    "properties": {
+        "context_summary": {"type": "string"},
+        "math_area": {"type": "array", "items": {"type": "string"}},
+        "techniques": {"type": "array", "items": {"type": "string"}},
+        "theorems_used": {"type": "array", "items": {"type": "string"}},
+        "difficulty": {"type": "integer"},
+        "keywords": {"type": "array", "items": {"type": "string"}},
+    },
+    "required": ["context_summary", "math_area", "techniques", "theorems_used", "difficulty", "keywords"],
+}
+_SPLIT_SCHEMA = {"type": "object", "properties": {"first_line": {"type": "string"}}, "required": ["first_line"]}
+
+
+class Enricher:
+    def __init__(self, cache_dir: str | Path, ingest_yaml: str = "configs/ingest.yaml", versions_yaml: str = "configs/versions.yaml", llm: LLM | None = None):
+        cfg = yaml.safe_load(open(ingest_yaml, encoding="utf-8"))["enrich"]
+        self.llm = llm or LLM(versions_yaml, section="vlm_enrichment")
+        self.prompts = cfg
+        self.version = str(cfg["prompt_version"])
+        self.cache_dir = Path(cache_dir)
+        self.cache_dir.mkdir(parents=True, exist_ok=True)
+        self._cache: dict[str, dict] = {}
+        self._lock = threading.Lock()
+
+    @property
+    def models(self) -> list[str]:
+        return self.llm.models
+
+    @property
+    def model(self) -> str:
+        return self.llm.model
+
+    @property
+    def exhausted(self) -> list[str]:
+        return self.llm.exhausted
+
+    @property
+    def calls(self) -> int:
+        return self.llm.calls
+
+    # -- caché ---------------------------------------------------------------
+
+    def _cache_file(self, op: str) -> Path:
+        return self.cache_dir / f"{op}.jsonl"
+
+    def _load(self, op: str) -> dict:
+        if op not in self._cache:
+            self._cache[op] = {}
+            f = self._cache_file(op)
+            if f.exists():
+                for line in f.read_text(encoding="utf-8").splitlines():
+                    if line.strip():
+                        rec = json.loads(line)
+                        self._cache[op][rec["key"]] = (rec["result"], rec.get("model", self.llm.models[0]))
+        return self._cache[op]
+
+    def _key(self, op: str, *parts: str) -> str:
+        # El prompt de la operación entra en la clave: editar un prompt invalida sólo su caché.
+        # El modelo NO entra: un resultado ya calculado por cualquier modelo de la cadena se reutiliza.
+        h = hashlib.sha256(("\x00".join([self.version, op, self.prompts.get(op, ""), *parts])).encode("utf-8"))
+        return h.hexdigest()[:24]
+
+    def _cached(self, op: str, key: str, compute) -> tuple:
+        """Devuelve (resultado, modelo que lo produjo)."""
+        with self._lock:
+            cache = self._load(op)
+            if key in cache:
+                return cache[key]
+        result, model = compute()  # fuera del lock: las llamadas HTTP corren en paralelo
+        with self._lock:
+            cache[key] = (result, model)
+            with self._cache_file(op).open("a", encoding="utf-8") as f:
+                f.write(json.dumps({"key": key, "model": model, "result": result}, ensure_ascii=False) + "\n")
+        return result, model
+
+    def map(self, fn, items, workers: int = 3) -> list:
+        """Aplica `fn` a `items` en paralelo (pocos hilos: la cuota es por minuto)."""
+        with ThreadPoolExecutor(max_workers=workers) as ex:
+            return list(ex.map(fn, items))
+
+    # -- llamadas (delegadas a ragsolver.llm.LLM) --------------------------------
+
+    def _generate(self, parts: list[dict], schema: dict | None) -> tuple[str, str]:
+        """(texto, modelo). `parts`: [{"text": ...}] y/o [{"image": path}]."""
+        prompt = "\n".join(p["text"] for p in parts if "text" in p)
+        images = [p["image"] for p in parts if "image" in p]
+        r = self.llm.generate(prompt, schema=schema, images=images)
+        return r.text, r.model
+
+    def _json(self, parts: list[dict], schema: dict) -> tuple[dict, str]:
+        text, model = self._generate(parts, schema)
+        return json.loads(text), model
+
+    # -- operaciones -----------------------------------------------------------
+
+    def transcribe_region(self, png_path: str | Path) -> str:
+        img = _image_part(png_path)
+        key = self._key("transcribe", _sha(png_path))
+        text, _ = self._cached("transcribe", key, lambda: (lambda t, m: (t.strip(), m))(*self._generate([{"text": self.prompts["transcribe"]}, img], None)))
+        return text
+
+    def describe_figure(self, png_path: str | Path, statement: str, solution: str = "") -> dict:
+        img = _image_part(png_path)
+        prompt = f"{self.prompts['figure']}\n\nProblem statement (Spanish):\n{statement}\n\nSolution excerpt (Spanish):\n{solution[:2500]}"
+        key = self._key("figure", _sha(png_path), statement, solution[:2500])
+        d, model = self._cached("figure", key, lambda: self._json([{"text": prompt}, img], _FIGURE_SCHEMA))
+        return {**d, "model": model}
+
+    def qa_formulas(self, page_png: str | Path, latex_list: list[str], inline: list[bool] | None = None) -> list[dict]:
+        """Devuelve [{i, latex, changed}] alineado con `latex_list`; `inline[i]` marca fórmulas en línea."""
+        if not latex_list:
+            return []
+        inline = inline or [False] * len(latex_list)
+        listing = "\n".join(f"[{i}] {s}" for i, s in enumerate(latex_list))
+        prompt = f"{self.prompts['formulas']}\n\n{listing}"
+        key = self._key("formulas", _sha(page_png), listing)
+        res, _ = self._cached("formulas", key, lambda: self._json([{"text": prompt}, _image_part(page_png)], _FORMULAS_SCHEMA))
+        out = [{"i": i, "latex": s, "changed": False} for i, s in enumerate(latex_list)]
+        for it in res.get("items", []):
+            i = it.get("i")
+            if not (isinstance(i, int) and 0 <= i < len(out) and it.get("changed")):
+                continue
+            if _alnum(it["latex"]) == _alnum(latex_list[i]):
+                continue  # cambio sólo de puntuación/espaciado: ruido, se ignora
+            if _acceptable_fix(latex_list[i], it["latex"], inline[i]):
+                out[i] = {"i": i, "latex": it["latex"], "changed": True}
+            else:
+                out[i]["rejected"] = it["latex"]
+        return out
+
+    def summarize_card(self, content_md: str, figure_descriptions: list[str]) -> dict:
+        prompt = self.prompts["card"].format(math_areas=", ".join(self.prompts["math_areas"]), techniques=", ".join(self.prompts["techniques"]))
+        figs = "\n".join(f"- {d}" for d in figure_descriptions) or "(none)"
+        body = f"{prompt}\n\n## Problem and solution (Spanish, Markdown+LaTeX)\n{content_md}\n\n## Figure descriptions\n{figs}"
+        key = self._key("card", content_md, figs)
+        res, model = self._cached("card", key, lambda: self._json([{"text": body}], _CARD_SCHEMA))
+        res = {**res, "model": model}
+        res["math_area"] = [a for a in res.get("math_area", []) if a in self.prompts["math_areas"]] or ["other"]
+        res["difficulty"] = min(5, max(1, int(res.get("difficulty", 3))))
+        return res
+
+    def split_solution(self, n: int, merged_text: str, statement_prev: str, statement_n: str) -> str:
+        prompt = self.prompts["split"].format(prev=n - 1, n=n)
+        body = f"{prompt}\n\n## Problem {n-1}\n{statement_prev}\n\n## Problem {n}\n{statement_n}\n\n## Text\n{merged_text}"
+        key = self._key("split", str(n), merged_text)
+        res, _ = self._cached("split", key, lambda: self._json([{"text": body}], _SPLIT_SCHEMA))
+        return res.get("first_line", "").strip()
+
+
+def _alnum(latex: str) -> str:
+    return re.sub(r"[^0-9A-Za-z^_{}]", "", latex)
+
+
+_CONTENT_RE = re.compile(r"[0-9+\-=<>/*]|\\(?:frac|sqrt|sum|prod|int|binom|cdot|times|le|ge|leq|geq|neq|equiv|in|pm|infty|angle|underbrace|overbrace)")
+
+
+def _garbage(chunk: str) -> bool:
+    """Trozo de LaTeX que se puede borrar sin perder matemática: envoltorios
+    (\\mathrm{...}, \\hat{...}) o texto absorbido por el OCR ("¿Cuál", "y"), sin
+    dígitos ni operadores."""
+    if _CONTENT_RE.search(chunk):
+        return False
+    letters = re.sub(r"[^A-Za-z]", "", re.sub(r"\\[A-Za-z]+", "", chunk))
+    return len(letters) <= 6
+
+
+def _canon(latex: str) -> str:
+    """Normaliza diferencias cosméticas antes de comparar (espacios, puntos suspensivos, espaciado LaTeX)."""
+    s = re.sub(r"\\[lc]?dots", "...", latex)
+    s = re.sub(r"\\[,;!:]|\\q?quad|~", "", s)
+    return re.sub(r"\s+", "", s)
+
+
+def _acceptable_fix(old_latex: str, new_latex: str, inline: bool) -> bool:
+    """Medido sobre el PDF de ejemplo (docs/DECISIONS.md #19): el VLM propone ruido de
+    puntuación, absorbe texto vecino en fórmulas inline, recorta contenido real cuando
+    el OCR fusionó texto+matemática, y a veces devuelve LaTeX destrozado (`\\underset`
+    -> `\\raw` con caracteres de control; `\\mathbb{R}` -> `ℒ`). Reglas:
+    (a) caracteres de control o no-ASCII nuevos -> rechazo;
+    (b) borrado puro -> aceptar sólo si cada trozo borrado es basura/envoltorio;
+    (c) otro cambio -> similitud >= 0.8 (arreglo local) y, en inline, no alargar."""
+    if re.search(r"[\x00-\x1f]", new_latex) or (set(new_latex) - set(old_latex)) & {c for c in new_latex if ord(c) > 127}:
+        return False
+    old, new = _canon(old_latex), _canon(new_latex)
+    if new == old or _alnum(new) == _alnum(old):
+        return False
+    ops = SequenceMatcher(None, old, new, autojunk=False).get_opcodes()
+    inserted = "".join(new[j1:j2] for tag, _, _, j1, j2 in ops if tag in ("insert", "replace"))
+    removed = [old[i1:i2] for tag, i1, i2, _, _ in ops if tag in ("delete", "replace")]
+    if not inserted:
+        return all(_garbage(chunk) for chunk in removed)
+    if inline and len(_alnum(new)) > len(_alnum(old)):
+        return False
+    return SequenceMatcher(None, old, new, autojunk=False).ratio() >= 0.8
+
+
+def _sha(path: str | Path) -> str:
+    return hashlib.sha256(Path(path).read_bytes()).hexdigest()[:16]
+
+
+def _image_part(path: str | Path) -> dict:
+    return {"image": str(path)}

ragsolver/rag/evaluate.py

@@ -0,0 +1,98 @@
+"""Fase 1, tarea 6 / Fase 3 aceptación — evaluación de retrieval sobre MathlibQR
+(docs/PLAN_RAG.md §10, §11).
+
+Compara 4 variantes (denso, BM25, híbrido, híbrido+rerank) con Recall@k/nDCG@10/MRR
+vía `rag/metrics.py` (no `ranx`: dos corridas largas del CLI devolvieron valores
+absurdos, docs/DECISIONS.md #43; `metrics.py` se verifica igual a `ranx` en
+`tests/test_metrics.py`), usando `full_name` de cada fila de MathlibQR como
+documento gold. Las cuatro variantes pasan por `Retriever.search` (la misma
+función que usan los agentes) — sólo cambian `channels` y `rerank`, no hay una
+segunda implementación de la búsqueda.
+
+IMPORTANTE: la cobertura (`n_gold_covered_in_table`) depende de la tabla que se
+evalúe. Con la muestra corregida (docs/DECISIONS.md #31-32, `mathlib_sample.jsonl`)
+la cobertura es 83.8 % (793/946); con el corpus completo (`mathlib_full`) el
+recall real baja a ~0.41-0.45 (#56, #68) — el número de la muestra sobreestima
+por el tamaño acotado del pool de candidatos, no sólo por cobertura.
+
+Uso: python -m ragsolver.rag.evaluate --qr data/eval/MathlibQR.json [--limit 20]
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import random
+import tempfile
+
+from ragsolver.rag.metrics import evaluate_run
+from ragsolver.rag.retrieve import Retriever
+from ragsolver.rag.schema import RetrievalRequest
+
+QUERY_FIELDS = ["q1a_lean", "q1b_latex", "q1c_natural", "q2_slogan", "q3_nickname", "q4_special_case"]
+
+VARIANTS = {  # nombre -> (canales, rerank)
+    "denso": (("dense",), False),
+    "bm25": (("sparse",), False),
+    "hibrido": (("dense", "sparse"), False),
+    "hibrido_rerank": (("dense", "sparse"), True),
+}
+
+
+def _build_queries(qr_path: str, limit: int | None = None, sample: int | None = None, seed: int = 13) -> list[dict]:
+    rows = json.load(open(qr_path, encoding="utf-8"))
+    queries = []
+    for row in rows:
+        gold_id = f"mathlib:{row['full_name']}:0"
+        for field in QUERY_FIELDS:
+            text = row.get(field, "")
+            if text:
+                queries.append({"query_id": f"{row['id']}:{field}", "text": text, "gold_id": gold_id})
+    if sample:  # subconjunto aleatorio reproducible (el rerank en CPU no alcanza para las 946)
+        queries = random.Random(seed).sample(queries, min(sample, len(queries)))
+    return queries[:limit] if limit else queries
+
+
+def evaluate_variants(retriever: Retriever, qr_path: str, table_name: str = "mathlib", n_candidates: int = 50, k: int = 10, limit: int | None = None, sample: int | None = None, variants: list[str] | None = None) -> dict:
+    queries = _build_queries(qr_path, limit, sample)
+    chosen = {name: VARIANTS[name] for name in (variants or VARIANTS)}
+    retriever.tables["mathlib"] = table_name  # la tabla evaluada sirve el corpus "mathlib"
+    table = retriever._table("mathlib")
+    all_ids = {r["chunk_id"] for r in table.search().select(["chunk_id"]).limit(table.count_rows()).to_list()}
+    n_covered = sum(1 for q in queries if q["gold_id"] in all_ids)
+    qrels = {q["query_id"]: {q["gold_id"]: 1} for q in queries}
+
+    retriever.trace_dir = tempfile.mkdtemp(prefix="ragsolver-eval-")  # no ensuciar data/eval/traces
+    runs: dict[str, dict] = {name: {} for name in chosen}
+    for q in queries:
+        for name, (channels, rerank) in chosen.items():
+            retriever.channels = channels
+            req = RetrievalRequest(queries=[q["text"]], corpora=["mathlib"], k=n_candidates, n_candidates=n_candidates, rerank=rerank, include_figures=False, context={"problem_id": "eval", "agent": "evaluate"})
+            hits = retriever.search(req).hits
+            runs[name][q["query_id"]] = {h.chunk_id: (h.citation.scores.rerank if rerank else h.citation.scores.fused) for h in hits}
+    retriever.channels = ("dense", "sparse")
+
+    return {
+        "n_queries": len(queries),
+        "n_gold_covered_in_table": n_covered,
+        "coverage_ratio": round(n_covered / len(queries), 3) if queries else 0.0,
+        **{name: evaluate_run(qrels, run, ks=(k,)) for name, run in runs.items()},
+        "_runs": runs,  # hits crudos por consulta: permiten recomputar las métricas sin repetir búsquedas
+    }
+
+
+if __name__ == "__main__":
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--db-path", default="data/index/lancedb")
+    ap.add_argument("--table", default="mathlib")
+    ap.add_argument("--qr", default="data/eval/MathlibQR.json")
+    ap.add_argument("--k", type=int, default=10)
+    ap.add_argument("--limit", type=int, default=None, help="evaluar sólo las primeras N consultas")
+    ap.add_argument("--sample", type=int, default=None, help="muestra aleatoria de N consultas (semilla fija)")
+    ap.add_argument("--variants", default=None, help="p.ej. denso,bm25,hibrido (por defecto las 4)")
+    ap.add_argument("--out", default=None, help="JSON con métricas y hits crudos (_runs)")
+    args = ap.parse_args()
+    out = evaluate_variants(Retriever(db_path=args.db_path), args.qr, args.table, k=args.k, limit=args.limit, sample=args.sample, variants=args.variants.split(",") if args.variants else None)
+    if args.out:
+        json.dump(out, open(args.out, "w", encoding="utf-8"), default=float)
+    print(json.dumps({k: v for k, v in out.items() if k != "_runs"}, indent=2, default=float))

ragsolver/rag/figures.py

@@ -0,0 +1,110 @@
+"""Fase 2, tareas 3-4 — recortes de figuras a partir de los bloques `image` de
+MinerU, unidos a la red de seguridad de clusters vectoriales (docs/PLAN_RAG.md §6.2).
+
+Un recorte por bloque imagen, con padding para que entren las etiquetas de los
+puntos (A, B, O...) que el PDF deja como texto suelto alrededor del dibujo.
+`figure_id = {doc_id}:fig:{page}:{block}` coincide con el locator markdown
+`.../page:{page}/block:{block}` que ya usa parse_structure, así el enlace
+figura <-> problem card no necesita nada más.
+"""
+
+from __future__ import annotations
+
+import hashlib
+from pathlib import Path
+
+import pymupdf
+
+from ragsolver.rag.ingest_pdf import detect_vector_figures
+from ragsolver.rag.mineru_blocks import _item_bboxes
+from ragsolver.rag.schema import Figure
+
+
+def _covered(rect: pymupdf.Rect, boxes: list[pymupdf.Rect]) -> float:
+    """Fracción de `rect` cubierta por la unión (aproximada por suma) de `boxes`."""
+    if rect.is_empty or rect.get_area() == 0:
+        return 0.0
+    area = sum((rect & b).get_area() for b in boxes if not (rect & b).is_empty)
+    return min(1.0, area / rect.get_area())
+
+
+def _crop(page: pymupdf.Page, rect: pymupdf.Rect, out: Path, dpi: int) -> str:
+    out.parent.mkdir(parents=True, exist_ok=True)
+    page.get_pixmap(dpi=dpi, clip=rect & page.rect).save(out)
+    return hashlib.sha256(out.read_bytes()).hexdigest()[:16]
+
+
+def crop_figures(
+    pdf_path: str | Path,
+    pages: dict[int, list[dict]],
+    out_dir: str | Path,
+    doc_id: str,
+    pad_pt: float = 10.0,
+    dpi: int = 200,
+    min_overlap: float = 0.6,
+) -> tuple[list[Figure], list[str]]:
+    """Devuelve (figuras, avisos). Avisos = clusters vectoriales que ningún bloque de
+    MinerU cubre (>= min_overlap): se recortan igual con detected_by=vector_cluster."""
+    doc = pymupdf.open(pdf_path)
+    out_dir = Path(out_dir)
+    vectors: dict[int, list[pymupdf.Rect]] = {}
+    for v in detect_vector_figures(pdf_path):
+        vectors.setdefault(v.page, []).append(pymupdf.Rect(*v.bbox))
+
+    figures: list[Figure] = []
+    warnings: list[str] = []
+    for pg in sorted(pages):
+        page = doc[pg - 1]
+        W, H = page.rect.width, page.rect.height
+        to_pt = lambda bb: pymupdf.Rect(bb[0] * W, bb[1] * H, bb[2] * W, bb[3] * H)
+        all_boxes = [to_pt(bb) for b in pages[pg] for bb in _item_bboxes(b)]
+        image_boxes = []
+        for b in pages[pg]:
+            if b["type"] not in ("image", "chart"):
+                continue
+            caption = " ".join(
+                it_c.get("content", "")
+                for it in b["content"] if it["type"] in ("image_caption", "image_footnote")
+                for it_c in it["content"]
+            ).strip()
+            for it in b["content"]:
+                if it["type"] not in ("image_body", "chart_body"):
+                    continue
+                rect = to_pt(it["bbox"])
+                image_boxes.append(rect)
+                padded = rect + (-pad_pt, -pad_pt, pad_pt, pad_pt)
+                block = it["index"] + 1
+                png = out_dir / f"p{pg:03d}_b{block}.png"
+                sha = _crop(page, padded, png, dpi)
+                has_vector = any(_covered(v, [rect]) >= min_overlap for v in vectors.get(pg, []))
+                figures.append(
+                    Figure(
+                        figure_id=f"{doc_id}:fig:{pg}:{block}",
+                        image_path=str(png),
+                        image_sha=sha,
+                        page=pg,
+                        bbox=[round(x, 4) for x in it["bbox"]],
+                        detected_by="both" if has_vector else "layout",
+                        caption=caption,
+                    )
+                )
+        # Red de seguridad: dibujo vectorial que MinerU no cubrió con ningún bloque
+        # (ni imagen, ni ecuación/texto — los radicales del Equation Editor caen en
+        # bloques equation/text y no cuentan como figura perdida).
+        for k, v in enumerate(vectors.get(pg, []), start=1):
+            if _covered(v, all_boxes) >= min_overlap:
+                continue
+            png = out_dir / f"p{pg:03d}_v{k}.png"
+            sha = _crop(page, v, png, dpi)
+            figures.append(
+                Figure(
+                    figure_id=f"{doc_id}:fig:{pg}:v{k}",
+                    image_path=str(png),
+                    image_sha=sha,
+                    page=pg,
+                    bbox=[round(v.x0 / W, 4), round(v.y0 / H, 4), round(v.x1 / W, 4), round(v.y1 / H, 4)],
+                    detected_by="vector_cluster",
+                )
+            )
+            warnings.append(f"página {pg}: cluster vectorial {tuple(round(x) for x in v)} sin bloque de MinerU -> {png.name}")
+    return figures, warnings

ragsolver/rag/index.py

@@ -0,0 +1,148 @@
+"""Índice LanceDB: construcción de tabla + búsqueda densa/FTS + fusión RRF.
+
+docs/PLAN_RAG.md §6.3 y §9.2. Una tabla por corpus (`mathlib`, `informal`).
+No hay clase "Store" genérica: son funciones sobre `lancedb.Table`, que ya es
+la abstracción — ponytail rung 2 (reusar lo que ya existe).
+"""
+
+from __future__ import annotations
+
+import json
+from pathlib import Path
+
+import lancedb
+from lancedb.index import FTS
+
+MATHLIB_FTS_COLUMNS = ["decl_name", "informal_name", "informal_description", "signature"]
+INFORMAL_FTS_COLUMNS = ["text", "keywords", "theorems_used"]
+
+_FTS_COLUMN = "_fts_text"  # columna derivada: lancedb >=0.25 sólo indexa FTS de a un campo
+
+
+def load_jsonl(path: str | Path) -> list[dict]:
+    rows = []
+    with open(path, encoding="utf-8") as f:
+        for line in f:
+            if line.strip():
+                rows.append(json.loads(line))
+    return rows
+
+
+def _write(db, table, table_name: str, batch: list[dict]):
+    if table is None:
+        return db.create_table(table_name, data=batch)
+    table.add(batch)  # devuelve un AddResult (truthy) en lancedb >= 0.25: no encadenar con `or`
+    return table
+
+
+def build_table(db_path: str, table_name: str, rows, fts_columns: list[str] | None = None, chunk: int = 5000) -> lancedb.table.Table:
+    """`fts_columns=None` crea una tabla de metadatos sin índice FTS (p.ej. `figures`).
+    `rows` puede ser un iterador (JSONL grande): se escribe por bloques de `chunk` filas."""
+    db = lancedb.connect(db_path)
+    if table_name in db.list_tables().tables:
+        db.drop_table(table_name)
+
+    def prep(row):
+        if fts_columns:
+            # lancedb >=0.25 sólo indexa FTS de un campo por índice; concatenamos las
+            # columnas buscables en una columna derivada en vez de mantener N índices.
+            return {**row, _FTS_COLUMN: " ".join(str(row.get(c, "")) for c in fts_columns)}
+        return row
+
+    table = None
+    batch: list[dict] = []
+    for row in rows:
+        batch.append(prep(row))
+        if len(batch) >= chunk:
+            table = _write(db, table, table_name, batch)
+            batch = []
+    if batch or table is None:
+        table = _write(db, table, table_name, batch)
+    if fts_columns:
+        table.create_index(_FTS_COLUMN, config=FTS())
+    return table
+
+
+def iter_jsonl(path: str | Path):
+    with open(path, encoding="utf-8") as f:
+        for line in f:
+            if line.strip():
+                yield json.loads(line)
+
+
+def open_table(db_path: str, table_name: str) -> lancedb.table.Table:
+    db = lancedb.connect(db_path)
+    return db.open_table(table_name)
+
+
+# Índice ANN (sólo tablas grandes, p.ej. `mathlib_full`): IVF con cuantización escalar de 8 bits y
+# re-ranking exacto de los `refine_factor × k` mejores → casi exacto con ~1 % de las lecturas. En la
+# búsqueda plana (sin índice) estos parámetros no tienen efecto. Ver DECISIONS #60.
+ANN_NPROBES = 32
+ANN_REFINE = 5
+
+
+def build_ann_index(table: lancedb.table.Table, num_partitions: int = 256) -> None:
+    table.create_index(metric="l2", vector_column_name="embedding", index_type="IVF_SQ", num_partitions=num_partitions, replace=True)
+
+
+def vector_search(table: lancedb.table.Table, query_vector: list[float], k: int, where: str | None = None) -> list[dict]:
+    q = table.search(query_vector, vector_column_name="embedding").nprobes(ANN_NPROBES).refine_factor(ANN_REFINE)
+    if where:
+        q = q.where(where, prefilter=True)
+    return q.limit(k).to_list()
+
+
+def fts_search(table: lancedb.table.Table, query_text: str, k: int, where: str | None = None) -> list[dict]:
+    q = table.search(query_text, query_type="fts", fts_columns=_FTS_COLUMN)
+    if where:
+        q = q.where(where, prefilter=True)
+    return q.limit(k).to_list()
+
+
+def sql_quote(value: str) -> str:
+    return "'" + str(value).replace("'", "''") + "'"
+
+
+def exact_match(table: lancedb.table.Table, column: str, values: list[str], where: str | None = None) -> list[dict]:
+    """Filas cuyo `column` es exactamente uno de `values` (modo `error`: identificador Lean literal)."""
+    if not values:
+        return []
+    expr = f"{column} IN ({', '.join(sql_quote(v) for v in values)})"
+    if where:
+        expr = f"({expr}) AND ({where})"
+    return table.search().where(expr).limit(len(values)).to_list()
+
+
+def rrf_fuse(ranked_lists: list[list[str]], k: int = 60) -> list[tuple[str, float]]:
+    """Reciprocal Rank Fusion estándar (docs/PLAN_RAG.md §6.3).
+
+    `ranked_lists`: una lista de listas de ids, ya ordenadas por relevancia
+    (rank 0 = mejor). Devuelve ids fusionados ordenados por score RRF desc.
+    """
+    scores: dict[str, float] = {}
+    for ranked in ranked_lists:
+        for rank, doc_id in enumerate(ranked):
+            scores[doc_id] = scores.get(doc_id, 0.0) + 1.0 / (k + rank + 1)
+    return sorted(scores.items(), key=lambda kv: kv[1], reverse=True)
+
+
+if __name__ == "__main__":
+    import argparse
+
+    ap = argparse.ArgumentParser(description="Construye (o reemplaza) una tabla LanceDB desde un JSONL embebido.")
+    ap.add_argument("--in", dest="in_path", default=None, help="p.ej. data/corpus/informal_embedded.jsonl (no hace falta con --ann-only)")
+    ap.add_argument("--table", required=True, choices=["mathlib", "mathlib_full", "informal", "figures"])
+    ap.add_argument("--db-path", default="data/index/lancedb")
+    ap.add_argument("--ann-only", action="store_true", help="no reconstruye: sólo crea el índice ANN (IVF_SQ) sobre la tabla existente")
+    args = ap.parse_args()
+    if args.ann_only:
+        table = lancedb.connect(args.db_path).open_table(args.table)
+        build_ann_index(table)
+        print(json.dumps({"table": args.table, "rows": table.count_rows(), "indices": [str(i.index_type) for i in table.list_indices()]}))
+        raise SystemExit
+    if not args.in_path:
+        ap.error("--in es obligatorio salvo con --ann-only")
+    fts = {"mathlib": MATHLIB_FTS_COLUMNS, "mathlib_full": MATHLIB_FTS_COLUMNS, "informal": INFORMAL_FTS_COLUMNS, "figures": None}[args.table]
+    table = build_table(args.db_path, args.table, iter_jsonl(args.in_path), fts_columns=fts)
+    print(json.dumps({"table": args.table, "rows": table.count_rows(), "db_path": args.db_path}))

ragsolver/rag/ingest_informal.py

@@ -0,0 +1,325 @@
+"""Fase 2 — Corpus B de punta a punta (docs/PLAN_RAG.md §6.2, tareas 3-9):
+
+  MinerU (JSON de bloques)
+    -> huecos del layout transcritos por VLM (Plan B acotado)
+    -> QA de fórmulas por página (6b)
+    -> Markdown regenerado -> problem cards (parse_structure)
+    -> soluciones con numeral perdido: split por LLM
+    -> recortes de figuras + descripciones (6a)
+    -> resumen contextual por card (6c)
+    -> chunks `problem_card` + `figure` -> data/corpus/informal.jsonl, figures.jsonl
+
+Idempotente: MinerU no se re-ejecuta (lee su salida ya guardada) y toda llamada
+al VLM/LLM queda cacheada en data/parsed/<doc_id>/enrich/. `--skip-llm` produce
+el corpus sin enriquecimiento (context_summary vacío), útil para tests.
+
+Uso: python -m ragsolver.rag.ingest_informal --pdf "problemas resueltos olimpiadas.pdf"
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+from pathlib import Path
+
+import pymupdf
+import yaml
+
+from ragsolver.rag.enrich import Enricher
+from ragsolver.rag.figures import crop_figures
+from ragsolver.rag.ingest_pdf import Inventory, inventory
+from ragsolver.rag.mineru_blocks import (
+    extract_item_numbers,
+    find_uncovered_regions,
+    image_locators,
+    insert_block,
+    load_pages,
+    render_markdown,
+    section_chunks,
+    text_block,
+)
+from ragsolver.rag.parse_structure import pair_problems_and_solutions, parse_markdown, split_item
+from ragsolver.rag.schema import Figure, InformalChunk
+
+
+def build_document_record(inv: Inventory, pdf_path: str) -> dict:
+    # Metadatos leídos del propio PDF (portada + metadata de Acrobat) durante el
+    # análisis inicial de la sesión de diseño — no vienen de un LLM.
+    return {
+        "doc_id": inv.doc_id,
+        "title": "Colectivo de Problemas resueltos para Estudiantes de Alto Rendimiento",
+        "authors": ["Miguel Angel Moreno Núñez", "Eduardo Tellechea Armenta"],
+        "year": 2002,
+        "source_type": "olympiad_collection",
+        "language": "es",
+        "file_path": pdf_path,
+        "sha256": inv.sha256,
+        "n_pages": inv.n_pages,
+        "license": "",
+        "redistributable": False,  # no se conoce la licencia -> no publicar en HF
+        "parser": "mineru",
+        "parser_version": "4.0.3",
+        "parser_tier": "standard",
+        "text_layer_reliable": inv.text_layer_reliable,
+        "index_version": "0.1.0",
+    }
+
+
+def _page_png(doc: pymupdf.Document, page: int, out_dir: Path, dpi: int, clip: pymupdf.Rect | None = None, name: str | None = None) -> Path:
+    out = out_dir / (name or f"page_{page:03d}.png")
+    if not out.exists():
+        out.parent.mkdir(parents=True, exist_ok=True)
+        doc[page - 1].get_pixmap(dpi=dpi, clip=clip).save(out)
+    return out
+
+
+def fill_gaps(pdf_path: str, pages: dict, enricher: Enricher, out_dir: Path, min_words: int, dpi: int) -> list[dict]:
+    """Plan B acotado: transcribe con el VLM las regiones que MinerU no cubrió y las
+    inserta como bloques de texto sintéticos en orden de lectura."""
+    doc = pymupdf.open(pdf_path)
+    log = []
+    for r in find_uncovered_regions(pdf_path, pages, min_words=min_words):
+        page = doc[r.page - 1]
+        W, H = page.rect.width, page.rect.height
+        x0, y0, x1, y1 = r.bbox
+        clip = pymupdf.Rect(0.08 * W, y0 - 6, 0.95 * W, y1 + 6)  # ancho completo de columna
+        png = _page_png(doc, r.page, out_dir / "gaps", dpi, clip=clip, name=f"gap_p{r.page:03d}.png")
+        md = enricher.transcribe_region(png)
+        insert_block(pages, r.page, text_block(md, [clip.x0 / W, clip.y0 / H, clip.x1 / W, clip.y1 / H]))
+        log.append({"page": r.page, "bbox_pt": [round(v) for v in r.bbox], "text_layer": r.words, "transcription": md})
+    return log
+
+
+def qa_formulas(pdf_path: str, pages: dict, enricher: Enricher, out_dir: Path, dpi: int) -> list[dict]:
+    """6b: por página con >= 1 ecuación, el VLM revisa el LaTeX contra la imagen.
+    Modifica los bloques in-place; devuelve el registro de cambios."""
+    doc = pymupdf.open(pdf_path)
+    jobs = []
+    for pg in sorted(pages):
+        refs: list[tuple[dict, bool]] = []  # (contenedor con clave "content", es inline)
+        for b in pages[pg]:
+            if b.get("synthetic"):
+                continue
+            if b["type"] == "equation":
+                refs.append((b, False))
+            elif isinstance(b.get("content"), list):
+                refs += [(it, True) for it in b["content"] if it.get("type") == "equation_inline"]
+        if refs:
+            jobs.append((pg, refs, _page_png(doc, pg, out_dir / "pages", dpi)))
+    results = enricher.map(lambda j: enricher.qa_formulas(j[2], [r["content"] for r, _ in j[1]], inline=[i for _, i in j[1]]), jobs)
+    diffs = []
+    for (pg, refs, _), items in zip(jobs, results):
+        for item in items:
+            ref, _ = refs[item["i"]]
+            if item["changed"]:
+                diffs.append({"page": pg, "before": ref["content"], "after": item["latex"]})
+                ref["content"] = item["latex"]
+            elif "rejected" in item:
+                diffs.append({"page": pg, "before": ref["content"], "rejected": item["rejected"]})
+    return diffs
+
+
+def recover_missing_solutions(parsed: dict, enricher: Enricher) -> list[str]:
+    """Soluciones cuyo numeral perdió el OCR: el LLM señala la primera línea dentro
+    de la solución anterior y `split_item` corta ahí (docs/PLAN_RAG.md: 'casos ambiguos')."""
+    problems = {p.number: p for p in parsed["problems"]}
+    solutions = {s.number: s for s in parsed["solutions"]}
+    notes = []
+    for n in sorted(problems):
+        if n in solutions or (n - 1) not in solutions:
+            continue
+        prev = solutions[n - 1]
+        first_line = enricher.split_solution(n, prev.text_md, problems[n - 1].text_md, problems[n].text_md)
+        res = split_item(prev, n, first_line) if first_line else None
+        if res is None:
+            notes.append(f"solución {n}: el LLM no encontró un corte verbatim ('{first_line[:60]}')")
+            continue
+        solutions[n - 1], solutions[n] = res
+        notes.append(f"solución {n}: recuperada por split de la {n - 1} en '{first_line[:60]}'")
+    parsed["solutions"] = [solutions[k] for k in sorted(solutions)]
+    return notes
+
+
+def build_chunks(cards: list[dict], figures_by_locator: dict[str, Figure], doc_id: str, enricher: Enricher | None) -> tuple[list[InformalChunk], list[Figure]]:
+    empty_meta = {"context_summary": "", "math_area": [], "techniques": [], "theorems_used": [], "difficulty": None, "keywords": []}
+    prepared = []
+    for card in cards:
+        n = card["item_number"]
+        prob, sol = card["problem"], card["solution"]
+        statement = prob.text_md if prob else ""
+        solution = sol.text_md if sol else ""
+        card_id = f"informal:{doc_id}:problem_card:{n}"
+        figs = [figures_by_locator[loc] for loc in card["image_locators"] if loc in figures_by_locator]
+        for f in figs:
+            f.linked_chunk_ids = [card_id]
+        prepared.append({"n": n, "prob": prob, "sol": sol, "statement": statement, "solution": solution, "card_id": card_id, "figs": figs})
+
+    if enricher is not None:  # 6a en paralelo
+        jobs = [(f, c["statement"], c["solution"]) for c in prepared for f in c["figs"]]
+
+        def _describe(job):
+            f, statement, solution = job
+            d = enricher.describe_figure(f.image_path, statement, solution)
+            f.description, f.labels, f.objects = d["description"], d["labels"], d["objects"]
+            f.relations, f.given_values, f.figure_type = d["relations"], d["given_values"], d["figure_type"]
+            f.description_model, f.description_version = d["model"], enricher.version
+
+        enricher.map(_describe, jobs)
+
+    for c in prepared:
+        parts = [c["statement"]] if c["statement"] else []
+        if c["solution"]:
+            parts.append("## Solución\n\n" + c["solution"])
+        if any(f.description for f in c["figs"]):
+            parts.append("## Figures\n\n" + "\n\n".join(f"[{f.figure_id}] {f.description}" for f in c["figs"] if f.description))
+        c["content_md"] = "\n\n".join(parts)
+
+    if enricher is not None:  # 6c en paralelo
+        metas = enricher.map(lambda c: enricher.summarize_card(c["content_md"], [f.description for f in c["figs"] if f.description]), prepared)
+    else:
+        metas = [dict(empty_meta) for _ in prepared]
+
+    chunks: list[InformalChunk] = []
+    used_figures: list[Figure] = []
+    for c, meta in zip(prepared, metas):
+        n, figs, card_id, content_md = c["n"], c["figs"], c["card_id"], c["content_md"]
+        used_figures += figs
+        text = (meta["context_summary"] + "\n\n" + content_md).strip()
+        pages = [p for item in (c["prob"], c["sol"]) if item for p in (item.page_start, item.page_end)]
+        chunks.append(
+            InformalChunk(
+                chunk_id=card_id,
+                doc_id=doc_id,
+                unit_type="problem_card",
+                text=text,
+                content_md=content_md,
+                context_summary=meta["context_summary"],
+                page_start=min(pages) if pages else None,
+                page_end=max(pages) if pages else None,
+                section_path=["Problemario", str(n)],
+                item_number=n,
+                math_area=meta["math_area"],
+                techniques=meta["techniques"],
+                theorems_used=meta["theorems_used"],
+                difficulty=meta["difficulty"],
+                keywords=meta["keywords"],
+                figure_ids=[f.figure_id for f in figs],
+                children_ids=[f"informal:{doc_id}:figure:{f.figure_id.rsplit(':fig:', 1)[1]}" for f in figs if f.description],
+                content_sha=hashlib.sha256(content_md.encode("utf-8")).hexdigest()[:16],
+                index_version="0.1.0",
+            )
+        )
+        for f in figs:
+            if not f.description:
+                continue
+            chunks.append(
+                InformalChunk(
+                    chunk_id=f"informal:{doc_id}:figure:{f.figure_id.rsplit(':fig:', 1)[1]}",
+                    doc_id=doc_id,
+                    unit_type="figure",
+                    text=f"{f.description}\n\nProblem: {c['statement']}",
+                    content_md=f.description,
+                    parent_id=card_id,
+                    page_start=f.page,
+                    page_end=f.page,
+                    bboxes=[[f.page, *f.bbox]],
+                    section_path=["Problemario", str(n)],
+                    item_number=n,
+                    language="en",
+                    math_area=meta["math_area"],
+                    keywords=f.labels + f.objects,
+                    figure_ids=[f.figure_id],
+                    content_sha=hashlib.sha256(f.description.encode("utf-8")).hexdigest()[:16],
+                    index_version="0.1.0",
+                )
+            )
+    return chunks, used_figures
+
+
+def run(pdf_path: str, mineru_dir: str | None = None, parsed_root: str = "data/parsed", corpus_dir: str = "data/corpus", skip_llm: bool = False, ingest_yaml: str = "configs/ingest.yaml", sections: str = "none") -> dict:
+    """`sections`: `none` (sólo problem cards), `front` (además, chunks `paper_section` de lo
+    anterior al Problemario), `all` (todo el documento por secciones: papers/apuntes)."""
+    cfg = yaml.safe_load(open(ingest_yaml, encoding="utf-8"))["pdf"]
+    inv = inventory(pdf_path)
+    doc_id = inv.doc_id
+    out_dir = Path(parsed_root) / doc_id
+    mineru_dir = mineru_dir or str(out_dir / "mineru")
+    pages = load_pages(mineru_dir)
+    report_numerals = extract_item_numbers(pages)
+    doc_short = doc_id[:7]  # MinerU usa los 7 primeros hex del sha256 en sus locators
+    enricher = None if skip_llm else Enricher(out_dir / "enrich")
+    report: dict = {"doc_id": doc_id, "n_pages": inv.n_pages, "item_numbers_from_equations": report_numerals}
+
+    if enricher is not None:
+        report["gaps"] = fill_gaps(pdf_path, pages, enricher, out_dir, cfg["gap_min_words"], cfg["render_dpi"])
+        report["formula_diffs"] = qa_formulas(pdf_path, pages, enricher, out_dir, cfg["render_dpi"])
+
+    md = render_markdown(pages, doc_short)
+    (out_dir / "full.fixed.md").write_text(md, encoding="utf-8")
+    parsed = parse_markdown(md)
+    if enricher is not None:
+        report["split_notes"] = recover_missing_solutions(parsed, enricher)
+    cards, warnings = pair_problems_and_solutions(parsed)
+
+    figures, fig_warnings = crop_figures(pdf_path, pages, out_dir / "figures", doc_id, pad_pt=cfg["figure_crop_padding_pt"], dpi=cfg["render_dpi"], min_overlap=cfg["vector_cluster_min_overlap"])
+    by_id = {f.figure_id: f for f in figures}
+    by_locator = {}
+    for loc, (pg, _) in image_locators(pages, doc_short).items():
+        fid = f"{doc_id}:fig:{pg}:{loc.rsplit(':', 1)[1]}"
+        if fid in by_id:
+            by_locator[loc] = by_id[fid]
+    # ponytail: figuras vectoriales no cubiertas por MinerU (ninguna en el PDF de ejemplo)
+    # se asignan al primer ítem cuyo rango de páginas las contiene; afinar por orden de
+    # lectura si aparece un corpus donde sí ocurra.
+    for f in figures:
+        if f.detected_by == "vector_cluster":
+            for card in cards:
+                items = [it for it in (card["problem"], card["solution"]) if it]
+                if any(it.page_start <= f.page <= it.page_end for it in items):
+                    loc = f"vector:{f.figure_id}"
+                    card["image_locators"].append(loc)
+                    by_locator[loc] = f
+                    break
+
+    chunks, used_figures = build_chunks(cards, by_locator, doc_id, enricher)
+    if sections != "none":  # docs/PLAN_RAG.md §6.2 paso 7: papers/apuntes -> paper_section (400-800 tokens)
+        for sc in section_chunks(md, doc_id, stop_at="Problemario" if sections == "front" else None):
+            chunks.append(InformalChunk(**sc, text=sc["content_md"], content_sha=hashlib.sha256(sc["content_md"].encode("utf-8")).hexdigest()[:16], index_version="0.1.0"))
+        report["n_sections"] = sum(1 for c in chunks if c.unit_type == "paper_section")
+
+    corpus = Path(corpus_dir)
+    corpus.mkdir(parents=True, exist_ok=True)
+    with (corpus / "informal.jsonl").open("w", encoding="utf-8") as f:
+        for c in chunks:
+            f.write(c.model_dump_json() + "\n")
+    with (corpus / "figures.jsonl").open("w", encoding="utf-8") as f:
+        for fig in used_figures:
+            f.write(fig.model_dump_json() + "\n")
+    (out_dir / "document.json").write_text(json.dumps(build_document_record(inv, pdf_path), ensure_ascii=False, indent=2), encoding="utf-8")
+
+    report.update(
+        n_cards=len(cards),
+        n_paired=sum(1 for c in cards if c["problem"] and c["solution"]),
+        n_chunks=len(chunks),
+        n_figures=len(used_figures),
+        n_figures_detected=len(figures),
+        figure_warnings=fig_warnings,
+        warnings=warnings,
+        llm_calls=enricher.calls if enricher else 0,
+        models_exhausted=enricher.exhausted if enricher else [],
+    )
+    (out_dir / "ingest_report.json").write_text(json.dumps(report, ensure_ascii=False, indent=2), encoding="utf-8")
+    return report
+
+
+if __name__ == "__main__":
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--pdf", default="problemas resueltos olimpiadas.pdf")
+    ap.add_argument("--mineru-dir", default=None, help="por defecto data/parsed/<doc_id>/mineru")
+    ap.add_argument("--skip-llm", action="store_true")
+    ap.add_argument("--sections", default="none", choices=["none", "front", "all"], help="chunks paper_section: none | front (antes del Problemario) | all (papers/apuntes)")
+    args = ap.parse_args()
+    rep = run(args.pdf, args.mineru_dir, skip_llm=args.skip_llm, sections=args.sections)
+    print(json.dumps({k: v for k, v in rep.items() if k not in ("gaps", "formula_diffs")}, indent=2, ensure_ascii=False))
+    print("gaps:", len(rep.get("gaps", [])), "formula_diffs:", len(rep.get("formula_diffs", [])))

ragsolver/rag/ingest_mathlib.py

@@ -0,0 +1,123 @@
+"""Fase 1 — Corpus A: normaliza el JSONL de LeanSearch v2 al esquema MathlibChunk.
+
+docs/PLAN_RAG.md §6.1. Entrada: `lsv2-mathlib-v4.28.0-rc1.jsonl` (310 579 registros,
+FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl, Apache-2.0). Salida: `data/corpus/mathlib.jsonl`
+con un `MathlibChunk` por línea (sin `embedding` todavía — eso lo hace `embed.py`).
+
+Uso: python -m ragsolver.rag.ingest_mathlib [--config configs/ingest.yaml] [--limit N]
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import re
+from pathlib import Path
+
+import yaml
+
+from ragsolver.rag.schema import MathlibChunk
+
+
+def _load_config(path: str) -> dict:
+    with open(path, encoding="utf-8") as f:
+        return yaml.safe_load(f)["mathlib"]
+
+
+def _should_exclude(record: dict, cfg: dict) -> bool:
+    if record.get("kind") in cfg["exclude_kinds"]:
+        return True
+    module_path = ".".join(record.get("module_name") or [])
+    if any(module_path.startswith(p) for p in cfg["exclude_module_prefixes"]):
+        return True
+    decl_name = ".".join(record.get("name") or [])
+    if any(sub in decl_name for sub in cfg["exclude_name_substrings"]):
+        return True
+    # lemas de ecuación autogenerados (`foo.eq_1`, `foo.eq_def`), sin borrar lemas reales como
+    # `Nat.Prime.eq_one_or_self_of_dvd` (docs/PLAN_MEJORA_RAG.md §2.4, Fase 3 tarea 4b)
+    if cfg.get("exclude_name_regex") and re.search(cfg["exclude_name_regex"], decl_name):
+        return True
+    return False
+
+
+def _docs_url(module_path: str, decl_name: str, base: str) -> str:
+    return f"{base}/{module_path.replace('.', '/')}.html#{decl_name}"
+
+
+def record_to_chunk(record: dict, cfg: dict, mathlib_tag: str, lean_version: str) -> MathlibChunk | None:
+    names = record.get("name") or []
+    if not names:
+        return None
+    # `name` es la lista de COMPONENTES del nombre (["GCDMonoid", "dvd_gcd"]), no
+    # alias: el nombre completo es su unión con "." (docs/DECISIONS.md #31).
+    decl_name = ".".join(names)
+    module_path = ".".join(record.get("module_name") or [])
+    informal_name = record.get("informal_name", "") or ""
+    informal_description = record.get("informal_description", "") or ""
+    signature = record.get("signature", "") or record.get("type", "") or ""
+
+    text = "\n".join(part for part in [informal_name, informal_description, "", signature] if part is not None).strip()
+    content_sha = hashlib.sha256(text.encode("utf-8")).hexdigest()[:16]
+
+    return MathlibChunk(
+        chunk_id=f"mathlib:{decl_name}:0",
+        doc_id=cfg["doc_id"],
+        text=text,
+        content_sha=content_sha,
+        decl_name=decl_name,
+        decl_names_alt=[],
+        module_path=module_path,
+        kind=record.get("kind", ""),
+        signature=signature,
+        type=record.get("type", "") or "",
+        value=record.get("value", "") or "",
+        informal_name=informal_name,
+        informal_description=informal_description,
+        mathlib_tag=mathlib_tag,
+        lean_version=lean_version,
+        docs_url=_docs_url(module_path, decl_name, cfg["docs_url_base"]),
+    )
+
+
+def run(config_path: str = "configs/ingest.yaml", versions_path: str = "configs/versions.yaml", limit: int | None = None) -> dict:
+    cfg = _load_config(config_path)
+    with open(versions_path, encoding="utf-8") as f:
+        versions = yaml.safe_load(f)
+    mathlib_tag = versions["lean"]["mathlib_tag"]
+    lean_version = versions["lean"]["toolchain"]
+
+    raw_path = Path(cfg["raw_jsonl"])
+    out_path = Path(cfg["out_jsonl"])
+    out_path.parent.mkdir(parents=True, exist_ok=True)
+
+    n_in = n_out = n_excluded = 0
+    with raw_path.open(encoding="utf-8") as fin, out_path.open("w", encoding="utf-8") as fout:
+        for line in fin:
+            if not line.strip():
+                continue
+            n_in += 1
+            if limit is not None and n_in > limit:
+                break
+            record = json.loads(line)
+            if _should_exclude(record, cfg):
+                n_excluded += 1
+                continue
+            chunk = record_to_chunk(record, cfg, mathlib_tag, lean_version)
+            if chunk is None:
+                n_excluded += 1
+                continue
+            fout.write(chunk.model_dump_json(exclude={"embedding"}) + "\n")
+            n_out += 1
+
+    return {"n_in": n_in, "n_out": n_out, "n_excluded": n_excluded, "out_path": str(out_path)}
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--config", default="configs/ingest.yaml")
+    parser.add_argument("--versions", default="configs/versions.yaml")
+    parser.add_argument("--limit", type=int, default=None, help="sólo las primeras N líneas del raw (debug)")
+    args = parser.parse_args()
+    stats = run(args.config, args.versions, args.limit)
+    print(json.dumps(stats, indent=2))

ragsolver/rag/ingest_pdf.py

@@ -0,0 +1,111 @@
+"""Fase 2 — Corpus B: inventario, render y red de seguridad de figuras vectoriales.
+
+docs/PLAN_RAG.md §6.2, Fase 2 tareas 1-4. El parseo estructural (MinerU +
+emparejamiento problema/solución) y el enriquecimiento VLM (tareas 5-6) van en
+módulos separados porque dependen de MinerU y de un proveedor de LLM/VLM
+respectivamente — ver docs/PROGRESS.md.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import re
+from dataclasses import dataclass
+from pathlib import Path
+
+import pymupdf
+
+# Heurística de fiabilidad de la capa de texto (docs/PLAN_RAG.md §3): líneas de
+# 1-2 caracteres sueltas y tokens matemáticos aislados delatan una capa de texto
+# que separó exponentes/subíndices de su base (p.ej. "2^2001" -> "22001").
+_SHORT_LINE_RE = re.compile(r"^\s*.{1,2}\s*$")
+
+
+def sha256_file(path: str | Path) -> str:
+    h = hashlib.sha256()
+    with open(path, "rb") as f:
+        for chunk in iter(lambda: f.read(1 << 20), b""):
+            h.update(chunk)
+    return h.hexdigest()
+
+
+@dataclass
+class Inventory:
+    doc_id: str
+    sha256: str
+    n_pages: int
+    text_layer_reliable: bool
+    short_line_ratio: float
+
+
+def inventory(pdf_path: str | Path) -> Inventory:
+    sha = sha256_file(pdf_path)
+    doc = pymupdf.open(pdf_path)
+    n_pages = len(doc)
+
+    total_lines = short_lines = 0
+    for page in doc:
+        for line in page.get_text().splitlines():
+            if not line.strip():
+                continue
+            total_lines += 1
+            if _SHORT_LINE_RE.match(line):
+                short_lines += 1
+    ratio = short_lines / total_lines if total_lines else 0.0
+
+    return Inventory(
+        doc_id=sha[:12],
+        sha256=sha,
+        n_pages=n_pages,
+        text_layer_reliable=ratio < 0.05,  # umbral conservador; documentos "limpios" están muy por debajo
+        short_line_ratio=round(ratio, 4),
+    )
+
+
+def render_pages(pdf_path: str | Path, out_dir: str | Path, dpi: int = 200) -> list[Path]:
+    out_dir = Path(out_dir)
+    out_dir.mkdir(parents=True, exist_ok=True)
+    doc = pymupdf.open(pdf_path)
+    paths = []
+    for i, page in enumerate(doc):
+        pix = page.get_pixmap(dpi=dpi)
+        p = out_dir / f"page_{i + 1:03d}.png"
+        pix.save(p)
+        paths.append(p)
+    return paths
+
+
+@dataclass
+class VectorFigure:
+    page: int  # 1-based
+    bbox: tuple[float, float, float, float]
+    n_paths: int
+
+
+def detect_vector_figures(pdf_path: str | Path, min_size_pt: float = 15.0, padding: float = 8.0) -> list[VectorFigure]:
+    """Red de seguridad de Fase 2, tarea 4: agrupa trazos vectoriales en figuras.
+
+    No depende de MinerU — se usa para verificar que MinerU no se comió ningún
+    diagrama de línea (docs/PLAN_RAG.md, riesgo "MinerU clasifica mal diagramas").
+
+    Filtra por tamaño mínimo (ambas dimensiones), no por cantidad de trazos: se
+    midió sobre el PDF de ejemplo (docs/DECISIONS.md) que diagramas geométricos
+    reales pueden tener sólo 2 trazos (un círculo + una línea), mientras que
+    reglas/subrayados decorativos con 1 solo trazo son anchos y muy bajos
+    (~12-15pt de alto). `min_size_pt=15` separa eso; recalibrar si se agregan
+    corpus con otro estilo de diagramación.
+    """
+    doc = pymupdf.open(pdf_path)
+    figures: list[VectorFigure] = []
+    for i, page in enumerate(doc):
+        drawings = page.get_drawings()
+        if not drawings:
+            continue
+        clusters = page.cluster_drawings(drawings=drawings)
+        for rect in clusters:
+            if min(rect.width, rect.height) < min_size_pt:
+                continue
+            padded = pymupdf.Rect(rect) + (-padding, -padding, padding, padding)
+            n_paths = sum(1 for d in drawings if padded.intersects(d["rect"]))
+            figures.append(VectorFigure(page=i + 1, bbox=tuple(padded), n_paths=n_paths))
+    return figures

ragsolver/rag/metrics.py

@@ -0,0 +1,39 @@
+"""Métricas de IR (docs/PLAN_RAG.md §11.2) sin dependencias: recall@k, nDCG@k (relevancia
+binaria, varios relevantes por consulta) y MRR. Reemplazan a `ranx` en las corridas
+largas: en dos corridas de evaluación `ranx` devolvió valores absurdos (recall 0.11 con
+las mismas listas de hits que, recomputadas desde las trazas, dan 0.76 —
+docs/DECISIONS.md #43). `tests/test_metrics.py` verifica la igualdad con ranx.
+"""
+
+from __future__ import annotations
+
+import math
+
+
+def ranked_ids(scored: dict[str, float]) -> list[str]:
+    return [d for d, _ in sorted(scored.items(), key=lambda kv: -kv[1])]
+
+
+def recall_at_k(ranked: list[str], relevant: set[str], k: int) -> float:
+    return len(relevant & set(ranked[:k])) / len(relevant) if relevant else 0.0
+
+
+def ndcg_at_k(ranked: list[str], relevant: set[str], k: int) -> float:
+    dcg = sum(1.0 / math.log2(i + 2) for i, d in enumerate(ranked[:k]) if d in relevant)
+    idcg = sum(1.0 / math.log2(i + 2) for i in range(min(len(relevant), k)))
+    return dcg / idcg if idcg else 0.0
+
+
+def mrr(ranked: list[str], relevant: set[str]) -> float:
+    return next((1.0 / (i + 1) for i, d in enumerate(ranked) if d in relevant), 0.0)
+
+
+def evaluate_run(qrels: dict[str, dict[str, int]], run: dict[str, dict[str, float]], ks: tuple[int, ...] = (10,)) -> dict[str, float]:
+    """Promedio sobre las consultas de `qrels` (consulta sin hits = 0, como ranx)."""
+    out: dict[str, float] = {}
+    n = len(qrels) or 1
+    for k in ks:
+        out[f"recall@{k}"] = sum(recall_at_k(ranked_ids(run.get(q, {})), set(rel), k) for q, rel in qrels.items()) / n
+        out[f"ndcg@{k}"] = sum(ndcg_at_k(ranked_ids(run.get(q, {})), set(rel), k) for q, rel in qrels.items()) / n
+    out["mrr"] = sum(mrr(ranked_ids(run.get(q, {})), set(rel)) for q, rel in qrels.items()) / n
+    return out

ragsolver/rag/mineru_blocks.py

@@ -0,0 +1,265 @@
+"""Fase 2 — lectura de la salida de MinerU 4 (esquema `docvortex.middle` 2.0).
+
+MinerU deja un JSON por rango de páginas con bloques tipados (text / equation /
+image / table / paragraph_title / ...) con bbox normalizado y contenido (LaTeX
+para ecuaciones). Este módulo:
+
+1. Carga esos bloques (`load_pages`).
+2. Cruza la capa de texto del PDF contra los bbox de MinerU para encontrar
+   contenido que el layout se saltó (`find_uncovered_regions`) — el PDF de
+   ejemplo perdió una solución entera (pág. 64) y varias líneas sueltas.
+   La capa de texto NO sirve para leer fórmulas (docs/PLAN_RAG.md §3), pero
+   sí para saber *dónde hay texto*.
+3. Regenera el Markdown con el mismo formato que `mineru-kit` (`render_markdown`),
+   para poder insertar bloques sintéticos (transcripciones VLM de las regiones
+   perdidas) y correcciones de LaTeX antes de parsear la estructura.
+
+Bloques sintéticos: dicts con la misma forma (`type`, `bbox`, `content`) más
+`synthetic: True`; `insert_block` los ubica por orden de lectura (y0).
+"""
+
+from __future__ import annotations
+
+import glob
+import json
+import re
+from dataclasses import dataclass
+from pathlib import Path
+
+import pymupdf
+
+# Numeral de ítem que MinerU absorbió dentro de una ecuación en display:
+#   "2 7. A = B", "\begin{array}{l} 5 2. \text{...}", "... \tag{88.}"
+# Sólo con el punto pegado al último dígito (un decimal espaciado sale "1 0 . 5").
+_LEADING_NUM_RE = re.compile(r"^(?:\\begin\{array\}\{[a-z ]*\}\s*)?(\d)(?:\s?(\d))?(?:\s?(\d))?\.\s+")
+_TAG_NUM_RE = re.compile(r"\\tag\s*\{(\d{1,3})\.\}\s*$")
+
+
+def load_pages(mineru_dir: str | Path) -> dict[int, list[dict]]:
+    """{página 1-based: [bloques en orden de lectura]} a partir de los *.json de MinerU."""
+    pages: dict[int, list[dict]] = {}
+    for f in sorted(glob.glob(str(Path(mineru_dir) / "*.json"))):
+        for p in json.load(open(f, encoding="utf-8"))["pages"]:
+            pages[p["page_idx"] + 1] = sorted(p["blocks"], key=lambda b: b["index"])
+    return pages
+
+
+def _item_bboxes(block: dict) -> list[list[float]]:
+    boxes = [block["bbox"]]
+    if isinstance(block.get("content"), list):
+        boxes += [it["bbox"] for it in block["content"] if isinstance(it, dict) and "bbox" in it]
+    return boxes
+
+
+@dataclass
+class UncoveredRegion:
+    page: int  # 1-based
+    bbox: tuple[float, float, float, float]  # puntos PDF
+    words: str
+
+
+def find_uncovered_regions(
+    pdf_path: str | Path, pages: dict[int, list[dict]], min_words: int = 4, tol_pt: float = 4.0
+) -> list[UncoveredRegion]:
+    """Palabras de la capa de texto cuyo centro no cae en ningún bbox de MinerU.
+
+    Una región por página (unión de las palabras sueltas); se ignora el pie de
+    página. `min_words` filtra ruido (separadores "* * *", etc.).
+    """
+    doc = pymupdf.open(pdf_path)
+    regions = []
+    for pg in range(1, len(doc) + 1):
+        page = doc[pg - 1]
+        W, H = page.rect.width, page.rect.height
+        boxes = [
+            pymupdf.Rect(x0 * W - tol_pt, y0 * H - tol_pt, x1 * W + tol_pt, y1 * H + tol_pt)
+            for b in pages.get(pg, [])
+            for x0, y0, x1, y1 in _item_bboxes(b)
+        ]
+        loose = []
+        for x0, y0, x1, y1, word, *_ in page.get_text("words"):
+            if y0 > 0.92 * H:
+                continue
+            c = pymupdf.Point((x0 + x1) / 2, (y0 + y1) / 2)
+            if not any(bx.contains(c) for bx in boxes):
+                loose.append((pymupdf.Rect(x0, y0, x1, y1), word))
+        if len(loose) >= min_words:
+            r = pymupdf.Rect(loose[0][0])
+            for rr, _ in loose[1:]:
+                r |= rr
+            regions.append(UncoveredRegion(pg, tuple(r), " ".join(w for _, w in loose)))
+    return regions
+
+
+def insert_block(pages: dict[int, list[dict]], page: int, block: dict) -> None:
+    """Inserta un bloque sintético en `page` por orden de lectura (y0 del bbox)."""
+    blocks = pages.setdefault(page, [])
+    y0 = block["bbox"][1]
+    pos = next((i for i, b in enumerate(blocks) if b["bbox"][1] > y0), len(blocks))
+    blocks.insert(pos, {**block, "synthetic": True})
+
+
+def text_block(text: str, bbox_norm: list[float]) -> dict:
+    return {"type": "text", "index": -1, "bbox": list(bbox_norm), "content": [{"type": "text", "content": text}]}
+
+
+# ---------------------------------------------------------------------------
+# Render Markdown (mismo formato que `mineru-kit`, ver data/parsed/*/full.md)
+# ---------------------------------------------------------------------------
+
+
+def _inline(items: list[dict]) -> str:
+    out = []
+    for it in items:
+        if it["type"] == "equation_inline":
+            out.append(f"${it['content']}$")
+        elif isinstance(it.get("content"), list):  # index: items anidados
+            out.append(_inline(it["content"]))
+        else:
+            s = it.get("content", "")
+            for style in it.get("styles", []):
+                s = {"bold": f"**{s}**", "superscript": f"<sup>{s}</sup>", "subscript": f"<sub>{s}</sub>"}.get(style, s)
+            out.append(s)
+    return "".join(out)
+
+
+def _table(html: str) -> str:
+    rows = [re.findall(r"<t[dh][^>]*>(.*?)</t[dh]>", r, flags=re.S) for r in re.findall(r"<tr[^>]*>(.*?)</tr>", html, flags=re.S)]
+    rows = [[c.strip() for c in r] for r in rows if r]
+    if not rows:
+        return html
+    width = max(len(r) for r in rows)
+    lines = ["| " + " | ".join(r + [""] * (width - len(r))) + " |" for r in rows]
+    lines.insert(1, "| " + " | ".join(["---"] * width) + " |")
+    return "\n".join(lines)
+
+
+def split_item_number(latex: str) -> tuple[int | None, str]:
+    """Devuelve (número de ítem, latex sin el numeral) si la ecuación lo absorbió."""
+    m = _LEADING_NUM_RE.match(latex)
+    if m:
+        n = int("".join(g for g in m.groups() if g))
+        prefix = latex[: m.start(1)]  # conserva un \begin{array} si lo había
+        return n, prefix + latex[m.end() :]
+    m = _TAG_NUM_RE.search(latex)
+    if m:
+        return int(m.group(1)), latex[: m.start()].rstrip()
+    return None, latex
+
+
+def extract_item_numbers(pages: dict[int, list[dict]]) -> list[tuple[int, int]]:
+    """Saca el numeral absorbido en ecuaciones a un bloque de texto propio ("N.")
+    justo antes. Correr ANTES de la QA de fórmulas (el VLM lo borra como basura)."""
+    found = []
+    for pg, blocks in pages.items():
+        i = 0
+        while i < len(blocks):
+            b = blocks[i]
+            if b["type"] == "equation":
+                n, latex = split_item_number(b["content"])
+                if n is not None:
+                    b["content"] = latex
+                    blocks.insert(i, {**text_block(f"{n}.", b["bbox"]), "synthetic": True})
+                    found.append((pg, n))
+                    i += 1
+            i += 1
+    return found
+
+
+def render_page(blocks: list[dict], page: int, n_pages: int, doc_short: str, tier: str) -> str:
+    parts = [f"<!-- page {page} of {n_pages} -->"]
+    for b in blocks:
+        t = b["type"]
+        if t == "page_number":
+            continue
+        if t in ("text",):
+            parts.append(_inline(b["content"]))
+        elif t in ("paragraph_title", "doc_title"):
+            level = 1 if t == "doc_title" else b.get("level", 2)
+            parts.append("#" * level + " " + _inline(b["content"]))
+        elif t == "equation":
+            parts.append(f"$$\n{b['content']}\n$$")
+        elif t in ("image", "chart"):
+            for it in b["content"]:
+                if it["type"] in ("image_body", "chart_body"):
+                    parts.append(f"![Image block](doc:{doc_short}/tier:{tier}/page:{page}/block:{it['index'] + 1})")
+                else:  # image_caption / image_footnote
+                    parts.append(_inline(it["content"]))
+        elif t == "table":
+            for it in b["content"]:
+                parts.append(_table(it["content"]) if it["type"] == "table_body" else _inline(it["content"]))
+        elif t == "index":
+            parts.append("\n".join(f"- {_inline([it])}" for it in b["content"]))
+        else:
+            parts.append(_inline(b["content"]) if isinstance(b["content"], list) else str(b["content"]))
+    return "\n\n".join(p for p in parts if p.strip())
+
+
+def render_markdown(pages: dict[int, list[dict]], doc_short: str, tier: str = "standard") -> str:
+    n = max(pages)
+    return "\n\n".join(render_page(pages[pg], pg, n, doc_short, tier) for pg in sorted(pages)) + "\n"
+
+
+def image_locators(pages: dict[int, list[dict]], doc_short: str, tier: str = "standard") -> dict[str, tuple[int, list[float]]]:
+    """{locator markdown: (página, bbox normalizado)} para cada image_body/chart_body."""
+    out = {}
+    for pg, blocks in pages.items():
+        for b in blocks:
+            if b["type"] in ("image", "chart"):
+                for it in b["content"]:
+                    if it["type"] in ("image_body", "chart_body"):
+                        out[f"doc:{doc_short}/tier:{tier}/page:{pg}/block:{it['index'] + 1}"] = (pg, it["bbox"])
+    return out
+
+
+# ---------------------------------------------------------------------------
+# Chunking por secciones (docs/PLAN_RAG.md §6.2, paso 7: papers/apuntes -> `paper_section`)
+# ---------------------------------------------------------------------------
+
+_HEADING_RE = re.compile(r"^(#{1,6})\s+(.*)$")
+
+
+def section_chunks(md_text: str, doc_id: str, max_chars: int = 3000, min_chars: int = 200, stop_at: str | None = None) -> list[dict]:
+    """Corta el Markdown en chunks `paper_section` de ~400-800 tokens (≈ `max_chars`) que
+    respetan párrafos y títulos; `section_path` = títulos vigentes; `page_start/end` desde
+    los marcadores `<!-- page N of T -->`. `stop_at`: título en el que se deja de cortar
+    (p.ej. "Problemario", cuyo contenido va por el camino de problem cards)."""
+    chunks: list[dict] = []
+    path: list[str] = []
+    page = 1
+    buf: list[str] = []
+    buf_pages: list[int] = []
+
+    def flush():
+        text = "\n\n".join(buf).strip()
+        if len(text) >= min_chars:
+            n = len(chunks)
+            chunks.append({"chunk_id": f"informal:{doc_id}:paper_section:{n}", "doc_id": doc_id, "unit_type": "paper_section", "section_path": list(path), "page_start": min(buf_pages), "page_end": max(buf_pages), "content_md": text, "order": n})
+        buf.clear()
+        buf_pages.clear()
+
+    for para in re.split(r"\n\s*\n", md_text):
+        para = para.strip()
+        if not para:
+            continue
+        pm = re.match(r"<!--\s*page (\d+) of \d+\s*-->", para)
+        if pm:
+            page = int(pm.group(1))
+            continue
+        hm = _HEADING_RE.match(para)
+        if hm:
+            title = hm.group(2).strip()
+            if stop_at and title.lower().startswith(stop_at.lower()):
+                break
+            flush()
+            level = len(hm.group(1))
+            path = path[: level - 1] + [title]
+            continue
+        if re.fullmatch(r"\d{1,3}", para):  # número de página suelto
+            continue
+        if buf and sum(len(p) for p in buf) + len(para) > max_chars:
+            flush()
+        buf.append(para)
+        buf_pages.append(page)
+    flush()
+    return chunks

ragsolver/rag/parse_structure.py

@@ -0,0 +1,168 @@
+"""Fase 2, tarea 5 — parser estructural sobre el Markdown de MinerU.
+
+Emparienta problema N (sección "Problemario") con su solución N (sección
+"Soluciones"), y extrae los locators de imagen (`doc:.../block:N`) que caen
+dentro de cada ítem. No usa LLM: es la ruta determinista que describe
+docs/PLAN_RAG.md §6.2 ("casos ambiguos -> una llamada LLM", que no aplica acá
+porque el documento tiene una estructura numerada regular).
+"""
+
+from __future__ import annotations
+
+import re
+from dataclasses import dataclass, field
+
+_PAGE_RE = re.compile(r"^<!--\s*page (\d+) of \d+\s*-->\s*$")
+# "21. texto", "## 21. texto", o "13." solo (la solución sigue en la línea siguiente,
+# frecuente cuando el ítem arranca directo con una fórmula en bloque).
+_ITEM_RE = re.compile(r"^(?:## )?(\d{1,3})\.\s*(?:\S.*)?$")
+_IMAGE_RE = re.compile(r"!\[Image block\]\((doc:[^)]+)\)")
+
+
+@dataclass
+class Item:
+    number: int
+    text_md: str
+    page_start: int
+    page_end: int
+    image_locators: list[str] = field(default_factory=list)
+
+
+def _split_section(lines: list[tuple[int, str]]) -> list[Item]:
+    """`lines`: [(page_num, line_text), ...] ya recortado a una sección.
+
+    Sólo se acepta un nuevo ítem si su número es >= el siguiente esperado
+    (no-decreciente, no estrictamente secuencial: a veces el número de un
+    ítem real queda atrapado dentro de una fórmula LaTeX -- p.ej. `\tag{100.}`
+    -- y ese ítem nunca hace match, lo cual no debe romper el resto de la
+    numeración). Rechazar los números MENORES al esperado es lo que evita que
+    un sub-caso dentro de una explicación (p.ej. "1. Prolongar el segmento
+    DC...", "2. Prolongar DA...") se confunda con el inicio de un ítem nuevo y
+    pise al ítem real con ese número -- pasó de verdad con la solución 1 en el
+    PDF de ejemplo (ver docs/DECISIONS.md).
+    """
+    items: list[Item] = []
+    current: list[tuple[int, str]] | None = None
+    current_number: int | None = None
+    expected = 1
+
+    # La sección "Soluciones" del PDF de ejemplo arranca con la solución 1 sin
+    # repetir el numeral: si el primer ítem numerado es el 2, lo que hay antes
+    # (salvo el título de sección) es el ítem 1.
+    first = next((i for i, (_, t) in enumerate(lines) if _ITEM_RE.match(t)), None)
+    if first is not None and int(_ITEM_RE.match(lines[first][1]).group(1)) == 2:
+        current, current_number, expected = [(p, t) for p, t in lines[:first] if not t.startswith("## ")], 1, 2
+        lines = lines[first:]
+
+    def flush():
+        nonlocal current, current_number
+        if current_number is not None and current:
+            text = "\n".join(t for _, t in current).strip()
+            pages = [p for p, _ in current]
+            images = _IMAGE_RE.findall(text)
+            items.append(Item(current_number, text, min(pages), max(pages), images))
+        current, current_number = [], None
+
+    for page, line in lines:
+        m = _ITEM_RE.match(line)
+        number = int(m.group(1)) if m else None
+        if number is not None and number >= expected:
+            flush()
+            current_number = number
+            expected = number + 1
+            current = [(page, line)]
+        elif current is not None:
+            current.append((page, line))
+    flush()
+    return items
+
+
+def parse_markdown(md_text: str) -> dict:
+    """Devuelve {"problems": [Item...], "solutions": [Item...], "warnings": [...]}."""
+    lines_with_page: list[tuple[int, str]] = []
+    page = 0
+    for raw_line in md_text.splitlines():
+        pm = _PAGE_RE.match(raw_line)
+        if pm:
+            page = int(pm.group(1))
+            continue
+        lines_with_page.append((page, raw_line))
+
+    full_text = "\n".join(t for _, t in lines_with_page)
+    idx_problemario = full_text.find("## Problemario")
+    idx_soluciones = full_text.find("## Soluciones")
+    idx_bibliografia = full_text.find("## Bibliografía")
+
+    warnings: list[str] = []
+    for name, idx in [("Problemario", idx_problemario), ("Soluciones", idx_soluciones), ("Bibliografía", idx_bibliografia)]:
+        if idx == -1:
+            warnings.append(f"sección '{name}' no encontrada")
+
+    def _char_offset_to_line_index(char_offset: int) -> int:
+        acc = 0
+        for i, (_, t) in enumerate(lines_with_page):
+            acc += len(t) + 1
+            if acc > char_offset:
+                return i
+        return len(lines_with_page)
+
+    i_problemario = _char_offset_to_line_index(idx_problemario) if idx_problemario >= 0 else 0
+    i_soluciones = _char_offset_to_line_index(idx_soluciones) if idx_soluciones >= 0 else len(lines_with_page)
+    i_bibliografia = _char_offset_to_line_index(idx_bibliografia) if idx_bibliografia >= 0 else len(lines_with_page)
+
+    problems = _split_section(lines_with_page[i_problemario:i_soluciones])
+    solutions = _split_section(lines_with_page[i_soluciones:i_bibliografia])
+
+    return {"problems": problems, "solutions": solutions, "warnings": warnings}
+
+
+def split_item(item: Item, n: int, first_line: str) -> tuple[Item, Item] | None:
+    """Parte `item` en (item, nuevo ítem `n`) en la línea `first_line` (verbatim).
+
+    Si esa línea está dentro de un bloque `$$`, el corte sube al `$$` de apertura.
+    Devuelve None si la línea no aparece. Los locators de imagen se reparten según
+    en qué mitad quedan.
+    """
+    lines = item.text_md.splitlines()
+    first_line = first_line.strip()
+    idx = next((i for i, l in enumerate(lines) if l.strip() == first_line), None)
+    if idx is None:
+        idx = next((i for i, l in enumerate(lines) if first_line and first_line in l), None)
+    if idx is None or idx == 0:
+        return None
+    opens = [i for i, l in enumerate(lines[:idx]) if l.strip() == "$$"]
+    if len(opens) % 2 == 1:  # dentro de un display: cortar en su apertura
+        idx = opens[-1]
+    head, tail = "\n".join(lines[:idx]).strip(), "\n".join(lines[idx:]).strip()
+    if not tail.startswith(f"{n}."):
+        tail = f"{n}.\n\n{tail}"
+    return (
+        Item(item.number, head, item.page_start, item.page_end, _IMAGE_RE.findall(head)),
+        Item(n, tail, item.page_start, item.page_end, _IMAGE_RE.findall(tail)),
+    )
+
+
+def pair_problems_and_solutions(parsed: dict) -> tuple[list[dict], list[str]]:
+    """Empareja por número. Devuelve (cards, warnings) — cards con problema+solución."""
+    problems_by_n = {p.number: p for p in parsed["problems"]}
+    solutions_by_n = {s.number: s for s in parsed["solutions"]}
+
+    warnings = list(parsed["warnings"])
+    all_numbers = sorted(set(problems_by_n) | set(solutions_by_n))
+    cards = []
+    for n in all_numbers:
+        prob = problems_by_n.get(n)
+        sol = solutions_by_n.get(n)
+        if prob is None:
+            warnings.append(f"solución {n} sin problema correspondiente")
+        if sol is None:
+            warnings.append(f"problema {n} sin solución correspondiente")
+        cards.append(
+            {
+                "item_number": n,
+                "problem": prob,
+                "solution": sol,
+                "image_locators": (prob.image_locators if prob else []) + (sol.image_locators if sol else []),
+            }
+        )
+    return cards, warnings

ragsolver/rag/premises.py

@@ -0,0 +1,128 @@
+"""Premisas por goal de Lean (docs/PLAN_MEJORA_RAG.md Fases 1, 3 y 4).
+
+El input del retrieval es el goal pretty-printed que devuelve el REPL en cada `sorry`, no el
+enunciado en lenguaje natural:
+- canal A, prior de competición: lemas por frecuencia en pruebas de Lean Workbook
+  (`scripts/build_premise_prior.py`), filtrados por los símbolos del goal;
+- canal B, selección nativa de Lean: se consume dentro de CLOSE (`grind +suggestions`), no como
+  lista de nombres (su lista para goals de competición es ruido: `not_fermat_42`, `BitVec.*`);
+- canal C, índice denso actual con el goal como consulta (`Retriever`, modo `formal`).
+A y C se fusionan con RRF. Todo cuesta 0 llamadas LLM.
+"""
+
+from __future__ import annotations
+
+import json
+import math
+import re
+from functools import lru_cache
+from itertools import combinations
+from pathlib import Path
+
+from ragsolver.rag.index import rrf_fuse
+
+PRIOR_PATH = "data/corpus/premise_prior.jsonl"
+
+IDENT_RE = re.compile(r"(?<![\w.'])([A-Za-z_][\w']*(?:\.[A-Za-z_][\w']*)*)")
+# palabras de tácticas y sintaxis que el regex de identificadores confunde con premisas
+TACTIC_WORDS = {
+    "by", "have", "exact", "apply", "intro", "intros", "rcases", "obtain", "refine", "refine'", "constructor", "simp", "simp_all", "norm_num", "linarith", "nlinarith",
+    "omega", "ring", "ring_nf", "field_simp", "positivity", "decide", "rfl", "use", "cases", "cases'", "induction", "induction'", "rw", "calc", "show", "fun", "at", "with",
+    "this", "norm_cast", "push_cast", "exact_mod_cast", "interval_cases", "by_contra", "by_cases", "push_neg", "split_ifs", "gcongr", "aesop", "tauto", "zify", "qify",
+    "simp_arith", "rw_mod_cast", "apply_fun", "native_decide", "nlinarith!", "linarith!", "contradiction", "exfalso", "assumption", "trivial", "specialize", "subst",
+}
+# `foo.mpr`, `foo.symm.le`: el lema es `foo`
+FIELD_SUFFIXES = {"mp", "mpr", "symm", "le", "lt", "ne", "ne'", "trans", "elim", "1", "2", "resolve_left", "resolve_right", "out", "mono", "ge", "gt", "not_lt", "not_le", "trans_le", "trans_lt"}
+# constantes de plomería que aparecen en `used_constants` de cualquier `rw`/`simp`/`linarith` y no son premisas
+PLUMBING_PREFIXES = ("Mathlib.Tactic.", "Mathlib.Meta.", "Lean.", "Std.Tactic.", "Aesop.", "Linarith.", "Nat.Linear.", "Int.Linear.", "Mathlib.Algebra.Order.Field.Basic.")
+PLUMBING = {"Eq.mpr", "Eq.mp", "congrArg", "congrFun", "congr", "id", "Eq.refl", "rfl", "of_eq_true", "eq_self", "propext", "Eq.trans", "Iff.refl", "trivial", "True.intro", "Eq.rec", "Eq.ndrec", "absurd", "Classical.byContradiction", "Decidable.byContradiction", "Not.intro", "eq_true", "eq_false", "False.elim", "id_eq", "Iff.intro", "And.intro"}
+_RELATION_RE = re.compile(r"[=≤<≥>≠↔∣∈∉¬∧∨]|\bFalse\b|\bTrue\b")
+# símbolos que "anclan" un lema a un dominio: si el lema los menciona y el goal no, no aplica
+SALIENT_RE = re.compile(r"[A-Z][\w']*(?:\.[\w']+)+|√|∑|∏|∣|%|!|⌊|⌈|ℕ|ℤ|ℝ|ℚ|ℂ|π|\blogb\b|\bchoose\b|\bgcd\b|\blcm\b|\babs\b|\|")
+_GENERIC_SALIENT = {"Nat.cast", "Int.cast", "OfNat.ofNat", "HPow.hPow", "HMul.hMul", "HAdd.hAdd", "HSub.hSub", "HDiv.hDiv"}
+
+
+def strip_field(name: str, known: set[str] | None = None) -> str:
+    """`sub_ne_zero.mpr` -> `sub_ne_zero` (si `known` se da, sólo cuando la base está en `known`)."""
+    parts = name.split(".")
+    while len(parts) > 1 and parts[-1] in FIELD_SUFFIXES:
+        parts.pop()
+        if known is not None and ".".join(parts) in known:
+            return ".".join(parts)
+    return ".".join(parts) if known is None else name
+
+
+def is_lemma_type(type_str: str) -> bool:
+    """Heurística: el tipo de un lema es una proposición (relación, conectivo); el de una definición
+    (`ℝ → ℝ`, `ℕ → ℕ → Prop`) no. ponytail: textual; `#print` exacto si aparecen falsos positivos."""
+    t = type_str.strip()
+    return bool(t) and not t.endswith("Prop") and not t.endswith("Type") and bool(_RELATION_RE.search(t))
+
+
+def is_premise_constant(name: str) -> bool:
+    return bool(name) and name not in PLUMBING and not name.startswith(PLUMBING_PREFIXES) and "._" not in name and ".match_" not in name and ".proof_" not in name and not name.split(".")[-1].startswith("inst")
+
+
+def proof_tokens(proof: str) -> set[str]:
+    """Identificadores candidatos a premisa en el cuerpo de una prueba (tras `:= by`), sin
+    tácticas ni accesos a campo; la validación contra Lean la hace quien llama."""
+    body = proof.split(":= by", 1)[1] if ":= by" in proof else proof
+    return {strip_field(t) for t in IDENT_RE.findall(body) if t not in TACTIC_WORDS and ("_" in t or "." in t) and len(t) > 3}
+
+
+def goal_target(goal: str) -> str:
+    """La meta de un goal pretty-printed (lo que sigue al último `⊢`)."""
+    return goal.rsplit("⊢", 1)[-1].strip()
+
+
+def salient(text: str) -> set[str]:
+    return {s for s in SALIENT_RE.findall(text) if s not in _GENERIC_SALIENT}
+
+
+@lru_cache(maxsize=2)
+def load_prior(path: str = PRIOR_PATH) -> tuple[dict, ...]:
+    p = Path(path)
+    if not p.exists():
+        return ()
+    rows = [json.loads(l) for l in p.read_text(encoding="utf-8").splitlines() if l.strip()]
+    for r in rows:
+        r["_salient"] = frozenset(salient(r.get("type", "")))
+    return tuple(rows)
+
+
+def prior_channel(goal: str, k: int = 32, prior: tuple[dict, ...] | None = None, filtered: bool = True) -> list[str]:
+    """Canal A: top-k del prior. `filtered`: descarta los lemas anclados a símbolos que el goal no
+    tiene (un lema de `√` no sirve para un goal de `%`); los genéricos (`sq_nonneg`) pasan siempre."""
+    prior = load_prior() if prior is None else prior
+    if not filtered:
+        return [r["decl_name"] for r in prior[:k]]
+    g = salient(goal)
+    return [r["decl_name"] for r in prior if r["_salient"] <= g][:k]
+
+
+def nlinarith_hints(goal: str, max_hints: int = 12) -> list[str]:
+    """Instancias de los lemas más frecuentes del prior (`sq_nonneg`, `mul_pos`) con las variables
+    del goal — el patrón `nlinarith [sq_nonneg (a - b), …]` de las pruebas de competición."""
+    hyps = [l for l in goal.split("⊢", 1)[0].splitlines() if " : " in l]
+    num_vars, pos_hyps = [], []
+    for l in hyps:
+        names, typ = l.split(" : ", 1)
+        typ = typ.strip()
+        if typ in ("ℝ", "ℚ", "ℤ", "ℕ"):
+            num_vars += names.split()
+        elif re.fullmatch(r"0 < [\w']+", typ) or re.fullmatch(r"[\w']+ > 0", typ):
+            pos_hyps += names.split()
+    hints = [f"sq_nonneg ({a} - {b})" for a, b in combinations(num_vars, 2)]
+    hints += [f"sq_nonneg ({a} + {b})" for a, b in combinations(num_vars, 2)]
+    hints += [f"mul_pos {a} {b}" for a, b in combinations(pos_hyps, 2)]
+    hints += [f"sq_nonneg {a}" for a in num_vars]
+    return hints[:max_hints]
+
+
+def fuse(*ranked: list[str], k: int = 16) -> list[str]:
+    """RRF de los canales (nombres de declaración), sin duplicados."""
+    return [n for n, _ in rrf_fuse([r for r in ranked if r], k=60)][:k]
+
+
+def log_prior(freq: int) -> float:
+    return math.log(max(freq, 1))

ragsolver/rag/proofs.py

@@ -0,0 +1,118 @@
+"""RAG de pruebas (DECISIONS #127): pruebas Lean verificadas de los problemas más parecidos al pedido.
+
+El RAG de lemas no le aporta al demostrador (los lemas genéricos ya los conoce, DECISIONS #109-#115); lo que
+le falta es cómo se resolvió un problema parecido (TacticToe, Tactician, Rango: recuperar pruebas, no sólo
+premisas). Corpus: Goedel-LM/Lean-workbook-proofs (29 750 pruebas verificadas, MIT; la misma descarga que el
+prior de `scripts/build_premise_prior.py`), sin las que coinciden con un enunciado de miniF2F. Se indexa el
+enunciado informal (el comentario `/- … -/`) + el enunciado Lean con Qwen3-Embedding, el modelo del resto del
+RAG, en la tabla `proofs`; la prueba va sin comentarios.
+
+Construcción: `python -m ragsolver.rag.proofs build` (con `RAGSOLVER_EMBED_BACKEND=llama`, minutos en la GPU).
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import re
+import textwrap
+from functools import lru_cache
+from pathlib import Path
+
+import yaml
+
+TABLE = "proofs"
+INSTRUCTION = "Given a competition mathematics problem, retrieve similar problems whose Lean 4 proofs use the same techniques"
+
+
+def _model() -> str:
+    return yaml.safe_load(open("configs/versions.yaml", encoding="utf-8"))["embedding"]["model"]
+
+
+def norm_statement(s: str) -> str:
+    """Enunciado sin nombre ni espacios redundantes (para excluir los de miniF2F, como el prior)."""
+    s = re.sub(r"^\s*theorem\s+\S+", "", s.split(":= by", 1)[0])
+    return re.sub(r"\s+", " ", s).strip()
+
+
+def parse(full_proof: str) -> dict | None:
+    """Archivo de Lean Workbook -> {informal, statement, proof}; None si no hay `theorem … := by`."""
+    i = full_proof.find("theorem")
+    m = re.search(r":=\s*by\b", full_proof[i:]) if i >= 0 else None
+    if not m:
+        return None
+    body = re.sub(r"/-.*?-/", "", full_proof[i + m.end() :], flags=re.S)
+    lines = [l for l in body.splitlines() if l.strip() and not l.strip().startswith("--")]
+    proof = textwrap.dedent("\n".join(lines)).strip()
+    if not proof:
+        return None
+    return {"informal": " ".join(re.findall(r"/-(.*?)-/", full_proof[:i], re.S)).strip(), "statement": full_proof[i : i + m.start()].strip(), "proof": proof}
+
+
+def build(parquet: str, db_path: str, minif2f: list[str]) -> dict:
+    import pyarrow.parquet as pq
+
+    from ragsolver.rag.embed import embed_documents
+    from ragsolver.rag.index import build_table
+
+    excluded = {norm_statement(json.loads(l)["formal_statement"]) for path in minif2f for l in open(path, encoding="utf-8")}
+    rows, n_excl = [], 0
+    for r in pq.read_table(parquet).to_pylist():
+        p = parse(r["full_proof"])
+        if p is None:
+            continue
+        if norm_statement(p["statement"]) in excluded:
+            n_excl += 1
+            continue
+        rows.append({"problem_id": r["problem_id"], **p})
+    vecs = embed_documents([f"{r['informal']}\n{r['statement']}"[:1500] for r in rows], _model())
+    build_table(db_path, TABLE, ({**r, "embedding": v} for r, v in zip(rows, vecs)), fts_columns=None)
+    return {"n_rows": len(rows), "n_excluded_minif2f": n_excl}
+
+
+@lru_cache(maxsize=1)
+def _table(db_path: str):
+    from ragsolver.rag.index import open_table
+
+    return open_table(db_path, TABLE)
+
+
+def similar(text: str, k: int = 3, max_sim: float = 0.95, db_path: str = "data/index/lancedb") -> list[dict]:
+    """Las k pruebas más parecidas a `text` (informal + enunciado Lean) con similitud coseno < `max_sim`:
+    por encima es el mismo problema (o casi) y la prueba sería la respuesta, no un ejemplo."""
+    from ragsolver.rag.embed import embed_queries
+    from ragsolver.rag.index import vector_search
+
+    q = embed_queries([text[:1500]], _model(), instruction=INSTRUCTION)[0]
+    out = []
+    for row in vector_search(_table(db_path), q, 4 * k):
+        sim = sum(a * b for a, b in zip(q, row["embedding"]))  # vectores normalizados
+        if sim < max_sim:
+            out.append({"problem_id": row["problem_id"], "statement": row["statement"], "proof": row["proof"], "sim": round(sim, 4)})
+        if len(out) == k:
+            break
+    return out
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser()
+    ap.add_argument("cmd", choices=["build", "preview"])
+    ap.add_argument("--parquet", default="data/raw/lean_workbook_proofs/data/train-00000-of-00001.parquet")
+    ap.add_argument("--minif2f", nargs="+", default=["data/eval/minif2f_v2/miniF2F_v2s.jsonl", "data/eval/minif2f_v2/miniF2F_v2c.jsonl"])
+    ap.add_argument("--db-path", default="data/index/lancedb")
+    ap.add_argument("--problems", nargs="*", default=[], help="preview: JSONL de problemas")
+    ap.add_argument("--max-sim", type=float, default=1.01)
+    args = ap.parse_args()
+    if args.cmd == "build":
+        print(json.dumps(build(args.parquet, args.db_path, args.minif2f)), flush=True)
+        return
+    for path in args.problems:  # preview: qué recuperaría cada problema (para revisar contaminación a mano)
+        for l in Path(path).read_text(encoding="utf-8").splitlines():
+            p = json.loads(l)
+            print(f"\n## {p['problem_id']}\n{p['formal_statement'][:300]}")
+            for h in similar(f"{p['informal_statement']}\n{p['formal_statement']}", 3, args.max_sim, args.db_path):
+                print(f"  [{h['sim']}] {h['problem_id']}: {h['statement'][:250]}")
+
+
+if __name__ == "__main__":
+    main()

ragsolver/rag/retrieve.py

@@ -0,0 +1,321 @@
+"""Fase 3 — Servicio de recuperación y citación (docs/PLAN_RAG.md §6.3, §6.4, §8).
+
+`Retriever.search(RetrievalRequest) -> RetrievalResult`:
+  plantilla por `mode` -> por consulta: denso top-N + FTS top-N (prefiltro SQL)
+  -> RRF multi-consulta y multi-canal -> rerank (cross-encoder) contra `rerank_against`
+  -> dedupe (figura vs. su problem card; máx. por módulo opcional) -> top-k
+  -> Citation[] + figuras adjuntas + evento JSONL.
+
+Modo `error`: los identificadores Lean del mensaje se buscan de forma exacta
+(`decl_name IN (...)`) y se fijan al tope del resultado; el resto de la consulta
+va por los canales normales. Costo en llamadas LLM: siempre 0 (RNF-3).
+"""
+
+from __future__ import annotations
+
+import os
+import re
+import time
+import uuid
+from functools import lru_cache
+from pathlib import Path
+
+import yaml
+
+from ragsolver.logging.jsonl_writer import append_event
+from ragsolver.rag.embed import embed_queries
+from ragsolver.rag.index import exact_match, fts_search, open_table, rrf_fuse, sql_quote, vector_search
+from ragsolver.rag.schema import (
+    Citation,
+    CitationScores,
+    Hit,
+    HitRecord,
+    RetrievalFilters,
+    RetrievalRequest,
+    RetrievalResult,
+    RetrievalTrace,
+    TraceEvent,
+    VersionsPin,
+)
+
+# `unknown identifier 'Nat.Prime.two_le'`, `unknown constant 'Foo.bar'`, `` `Foo.bar` ``
+_QUOTED_IDENT_RE = re.compile(r"(?:identifier|constant|namespace|declaration)\s+'([^']+)'|`([^`\s]+)`")
+_DOTTED_IDENT_RE = re.compile(r"\b[A-Z][A-Za-z0-9_']*(?:\.[A-Za-z0-9_']+)+\b")
+
+
+def lean_identifiers(text: str) -> list[str]:
+    """Identificadores Lean citados en un mensaje de error (sin duplicados, en orden)."""
+    found = [a or b for a, b in _QUOTED_IDENT_RE.findall(text)]
+    found += _DOTTED_IDENT_RE.findall(_QUOTED_IDENT_RE.sub(" ", text))  # los citados ya están; evita `Baz.qux` de `Baz.qux'`
+    return list(dict.fromkeys(f for f in found if f))
+
+
+def _mathlib_citation_label(row: dict) -> str:
+    return f"{row.get('decl_name', '?')} — {row.get('module_path', '?')}"
+
+
+def _mathlib_locator(row: dict) -> dict:
+    return {
+        "decl_name": row.get("decl_name"),
+        "module_path": row.get("module_path"),
+        "docs_url": row.get("docs_url"),
+    }
+
+
+def _informal_citation_label(row: dict) -> str:
+    item = row.get("item_number")
+    page = row.get("page_start")
+    suffix = f", ítem {item}" if item else ""
+    suffix += f", p. {page}" if page else ""
+    return f"{row.get('doc_id', '?')}{suffix}"
+
+
+def _informal_locator(row: dict) -> dict:
+    return {
+        "doc_id": row.get("doc_id"),
+        "page_start": row.get("page_start"),
+        "page_end": row.get("page_end"),
+        "item_number": row.get("item_number"),
+        "figure_ids": list(row.get("figure_ids") or []),
+    }
+
+
+_LABEL_BUILDERS = {"mathlib": _mathlib_citation_label, "informal": _informal_citation_label}
+_LOCATOR_BUILDERS = {"mathlib": _mathlib_locator, "informal": _informal_locator}
+
+
+def mathlib_table_name() -> str:
+    """MET-1: qué tabla LanceDB sirve el corpus `mathlib` — misma fuente de verdad
+    para el `Retriever` y para el pin de versiones que registran los agentes."""
+    return os.environ.get("RAGSOLVER_MATHLIB_TABLE", "mathlib")
+
+
+def sql_filter(corpus: str, filters: RetrievalFilters) -> str | None:
+    """Prefiltro SQL de LanceDB a partir de §8.1 `filters` (sólo los campos que aplican al corpus)."""
+    clauses = []
+    if filters.doc_ids:
+        clauses.append(f"doc_id IN ({', '.join(sql_quote(d) for d in filters.doc_ids)})")
+    if filters.unit_types:
+        clauses.append(f"unit_type IN ({', '.join(sql_quote(u) for u in filters.unit_types)})")
+    if corpus == "mathlib" and filters.kinds:
+        clauses.append(f"kind IN ({', '.join(sql_quote(k) for k in filters.kinds)})")
+    if corpus == "informal" and filters.math_area:
+        clauses.append(f"array_has_any(math_area, [{', '.join(sql_quote(a) for a in filters.math_area)}])")
+    return " AND ".join(clauses) or None
+
+
+class Retriever:
+    def __init__(self, db_path: str = "data/index/lancedb", versions_path: str = "configs/versions.yaml", config_path: str = "configs/retrieval.yaml"):
+        self.db_path = db_path
+        self.versions = yaml.safe_load(open(versions_path, encoding="utf-8"))
+        self.config = yaml.safe_load(open(config_path, encoding="utf-8")) if Path(config_path).exists() else {}
+        self.channels: tuple[str, ...] = ("dense", "sparse")  # sólo para ablaciones de evaluate.py
+        self.trace_dir = "data/eval/traces"
+        # el corpus "mathlib" puede servirse desde otra tabla (p.ej. `mathlib_full`, 278k) sin tocar filtros ni citas
+        self.tables = {"mathlib": mathlib_table_name()}
+
+    @lru_cache(maxsize=8)
+    def _table(self, name: str):
+        return open_table(self.db_path, self.tables.get(name, name))
+
+    @lru_cache(maxsize=1)
+    def _reranker(self):
+        import torch
+        from sentence_transformers import CrossEncoder
+
+        # bf16 en CPU: mitad de RAM que fp32 (docs/DECISIONS.md #40); RAGSOLVER_EMBED_BF16=0 restaura fp32
+        dtype = torch.bfloat16 if os.environ.get("RAGSOLVER_EMBED_BF16", "1") == "1" else torch.float32
+        return CrossEncoder(self.versions["reranker"]["model"], device="cpu", model_kwargs={"torch_dtype": dtype})
+
+    # -- candidatos ------------------------------------------------------------
+
+    def _candidates(self, corpus: str, request: RetrievalRequest) -> tuple[dict, list[list[str]], list[str]]:
+        """(filas por id, listas rankeadas para RRF, ids fijados al tope)."""
+        table = self._table(corpus)
+        where = sql_filter(corpus, request.filters)
+        instruction = (self.config.get("query_instructions") or {}).get(request.mode)
+        rows_by_id: dict = {}
+        ranked: list[list[str]] = []
+        pinned: list[str] = []
+
+        if request.mode == "error" and corpus == "mathlib":
+            idents = [i for q in request.queries for i in lean_identifiers(q)]
+            for row in exact_match(table, "decl_name", idents, where):
+                rows_by_id.setdefault(row["chunk_id"], row)
+                pinned.append(row["chunk_id"])
+            if idents:  # tokens del identificador ("Nat Prime two_le") como consulta FTS extra
+                sparse = fts_search(table, " ".join(re.sub(r"[._']", " ", i) for i in idents), request.n_candidates, where)
+                for row in sparse:
+                    rows_by_id.setdefault(row["chunk_id"], row)
+                ranked.append([r["chunk_id"] for r in sparse])
+
+        vectors = embed_queries(request.queries, model_name=self.versions["embedding"]["model"], instruction=instruction) if "dense" in self.channels else [None] * len(request.queries)
+        for q_text, q_vec in zip(request.queries, vectors):
+            if "dense" in self.channels:
+                dense = vector_search(table, q_vec, request.n_candidates, where)
+                for row in dense:
+                    rows_by_id.setdefault(row["chunk_id"], row)
+                ranked.append([r["chunk_id"] for r in dense])
+            if "sparse" in self.channels:
+                sparse = fts_search(table, q_text, request.n_candidates, where)
+                for row in sparse:
+                    rows_by_id.setdefault(row["chunk_id"], row)
+                ranked.append([r["chunk_id"] for r in sparse])
+        return rows_by_id, ranked, list(dict.fromkeys(pinned))
+
+    # -- dedupe ------------------------------------------------------------------
+
+    def _dedupe(self, corpus: str, rows: list[dict]) -> list[dict]:
+        out: list[dict] = []
+        if corpus == "informal":
+            # figura cuyo problem card también fue recuperado: se colapsa en el card
+            # (que ya lleva `figure_ids`); la figura sola sigue siendo un hit válido.
+            ids = {r["chunk_id"] for r in rows}
+            rows = [r for r in rows if not (r.get("unit_type") == "figure" and r.get("parent_id") in ids)]
+        per_module: dict[str, int] = {}
+        limit = int(self.config.get("max_per_module") or 0)
+        for r in rows:
+            if corpus == "mathlib" and limit:
+                m = r.get("module_path", "")
+                per_module[m] = per_module.get(m, 0) + 1
+                if per_module[m] > limit:
+                    continue
+            out.append(r)
+        return out
+
+    def _figures(self, figure_ids: list[str]) -> list[dict]:
+        if not figure_ids:
+            return []
+        try:
+            table = self._table("figures")
+        except Exception:  # tabla `figures` ausente (índice construido sin corpus informal)
+            return []
+        rows = exact_match(table, "figure_id", figure_ids)
+        keep = ("figure_id", "image_path", "description", "page", "bbox", "figure_type", "labels")
+        return [{k: r.get(k) for k in keep} for r in rows]
+
+    # -- búsqueda ----------------------------------------------------------------
+
+    def search(self, request: RetrievalRequest) -> RetrievalResult:
+        t0 = time.time()
+        ablation = self.config.get("ablation") or {}
+        corpora = [c for c in request.corpora if c in (ablation.get("corpora") or request.corpora)]
+        if ablation.get("enabled", True) is False:
+            corpora = []
+
+        all_hits: list[Hit] = []
+        for corpus in corpora:
+            rows_by_id, ranked, pinned = self._candidates(corpus, request)
+            fused = rrf_fuse(ranked, k=int(self.config.get("rrf_k", 60)))
+            fused_score = dict(fused)
+            order_ids = pinned + [cid for cid, _ in fused if cid not in pinned]
+            candidates = self._dedupe(corpus, [rows_by_id[c] for c in order_ids if c in rows_by_id])[: request.n_candidates]
+
+            rerank_scores: dict[str, float] = {}
+            if request.rerank and candidates:
+                against = request.rerank_against or request.queries[0]
+                scores = self._reranker().predict([(against, r["text"]) for r in candidates])
+                rerank_scores = {r["chunk_id"]: float(s) for r, s in zip(candidates, scores)}
+                unpinned = sorted((r for r in candidates if r["chunk_id"] not in pinned), key=lambda r: rerank_scores[r["chunk_id"]], reverse=True)
+                candidates = [r for r in candidates if r["chunk_id"] in pinned] + unpinned
+
+            prefix = "M" if corpus == "mathlib" else "I"
+            for rank, row in enumerate(candidates[: request.k], start=1):
+                cid = row["chunk_id"]
+                citation = Citation(
+                    citation_id=f"{prefix}{rank}",
+                    chunk_id=cid,
+                    corpus=corpus,
+                    unit_type=row.get("unit_type", ""),
+                    label=_LABEL_BUILDERS[corpus](row),
+                    locator=_LOCATOR_BUILDERS[corpus](row),
+                    scores=CitationScores(fused=fused_score.get(cid), rerank=rerank_scores.get(cid)),
+                    retrieved_for=request.context,
+                    snippet=(row.get("content_md") or row.get("text") or "")[:300],
+                )
+                figures = self._figures(list(row.get("figure_ids") or [])) if (corpus == "informal" and request.include_figures) else []
+                all_hits.append(
+                    Hit(
+                        chunk_id=cid,
+                        corpus=corpus,
+                        unit_type=row.get("unit_type", ""),
+                        rank=rank,
+                        text=row.get("text", ""),
+                        content_md=row.get("content_md", ""),
+                        metadata={k: v for k, v in row.items() if k not in ("embedding", "text", "content_md", "_fts_text", "_distance", "_score")},
+                        figures=figures,
+                        citation=citation,
+                    )
+                )
+
+        latency_ms = (time.time() - t0) * 1000
+        pin = VersionsPin(
+            embedding_model=self.versions["embedding"]["model"],
+            reranker_model=self.versions["reranker"]["model"],
+            index_version=self.versions["index"]["version"],
+            mathlib_tag=self.versions["lean"]["mathlib_tag"],
+            mathlib_table=self.tables.get("mathlib", "mathlib"),
+        )
+        # TRZ-1: si el llamador pasa `context.run_id` (el orquestador pasa el pid de la corrida), el
+        # evento va al MISMO archivo que los eventos de los agentes de ese (config, problema) en vez
+        # de crear un archivo nuevo por búsqueda. Sin run_id (CLI, demo, evaluate.py) se mantiene el
+        # comportamiento anterior: un archivo por búsqueda, con sufijo aleatorio.
+        append_event(
+            TraceEvent(
+                run_id=request.context.run_id or f"{request.context.problem_id}:{uuid.uuid4().hex[:8]}",
+                problem_id=request.context.problem_id,
+                subgoal_id=request.context.subgoal_id,
+                attempt=request.context.attempt,
+                agent="retriever",
+                latency_ms=latency_ms,
+                llm_calls=0,
+                request=request.model_dump(mode="json"),
+                n_candidates=request.n_candidates,
+                hits=[HitRecord(chunk_id=h.chunk_id, rank=h.rank, scores=h.citation.scores) for h in all_hits],
+                versions=pin,
+            ),
+            base_dir=self.trace_dir,
+        )
+        return RetrievalResult(
+            hits=all_hits,
+            citations=[h.citation for h in all_hits],
+            trace=RetrievalTrace(latency_ms=latency_ms, n_candidates=request.n_candidates, versions=pin),
+        )
+
+
+def _cli(argv: list[str] | None = None) -> None:
+    """`ragsolver search "query" --corpus mathlib --k 8` (docs/PLAN_RAG.md Fase 3, tarea 7)."""
+    import argparse
+    import json as _json
+
+    ap = argparse.ArgumentParser(prog="ragsolver search")
+    ap.add_argument("query", nargs="+", help="una o más consultas (se fusionan con RRF)")
+    ap.add_argument("--corpus", action="append", choices=["mathlib", "informal"], help="repetible; por defecto mathlib")
+    ap.add_argument("--mode", default="nl", choices=["nl", "formal", "error", "exemplar"])
+    ap.add_argument("--k", type=int, default=8)
+    ap.add_argument("--no-rerank", action="store_true")
+    ap.add_argument("--math-area", action="append", default=[])
+    ap.add_argument("--db-path", default="data/index/lancedb")
+    args = ap.parse_args(argv)
+
+    req = RetrievalRequest(
+        queries=args.query,
+        mode=args.mode,
+        corpora=args.corpus or ["mathlib"],
+        k=args.k,
+        rerank=not args.no_rerank,
+        filters={"math_area": args.math_area},
+        context={"problem_id": "cli", "agent": "cli"},
+    )
+    result = Retriever(db_path=args.db_path).search(req)
+    for hit in result.hits:
+        sc = hit.citation.scores
+        print(f"[{hit.citation.citation_id}] {hit.citation.label}  (fused={sc.fused and round(sc.fused, 4)}, rerank={sc.rerank and round(sc.rerank, 3)})")
+        print(f"    {hit.text[:160]!r}")
+        for fig in hit.figures:
+            print(f"    fig {fig['figure_id']}: {fig['image_path']} — {(fig['description'] or '')[:100]!r}")
+    print(_json.dumps({"latency_ms": round(result.trace.latency_ms, 1), "n_hits": len(result.hits)}))
+
+
+if __name__ == "__main__":
+    _cli()

ragsolver/rag/schema.py

@@ -0,0 +1,246 @@
+"""Contratos tipados del módulo RAG (RNF-4).
+
+Espejo exacto de docs/PLAN_RAG.md §7 (esquema de metadatos) y §8 (contratos del
+recuperador). No importar nada de ragsolver.agents/ragsolver.orchestrator desde
+aquí — el RAG es una capa independiente que los agentes consumen (docs/PLAN_RAG.md §0).
+"""
+
+from __future__ import annotations
+
+from datetime import datetime, timezone
+from typing import Literal
+
+from pydantic import BaseModel, Field
+
+Corpus = Literal["mathlib", "informal"]
+QueryMode = Literal["nl", "formal", "error", "exemplar"]
+
+# ---------------------------------------------------------------------------
+# §7.1 — documents
+# ---------------------------------------------------------------------------
+
+
+class Document(BaseModel):
+    doc_id: str
+    title: str = ""
+    authors: list[str] = Field(default_factory=list)
+    year: int | None = None
+    source_type: Literal["olympiad_collection", "paper", "textbook", "notes", "mathlib"]
+    language: str = "en"
+    file_path: str = ""
+    sha256: str = ""
+    n_pages: int = 0
+    url: str = ""
+    license: str = ""
+    redistributable: bool = False
+    parser: str = ""
+    parser_version: str = ""
+    parser_tier: str = ""
+    text_layer_reliable: bool | None = None
+    ingested_at: str = Field(default_factory=lambda: datetime.now(timezone.utc).isoformat())
+    index_version: str = ""
+
+
+# ---------------------------------------------------------------------------
+# §7.2 — chunks (núcleo común) + §7.3/§7.4 extensiones por corpus
+# ---------------------------------------------------------------------------
+
+
+class ChunkBase(BaseModel):
+    """Campos comunes a las dos tablas LanceDB (`mathlib`, `informal`)."""
+
+    chunk_id: str
+    doc_id: str
+    corpus: Corpus
+    unit_type: str
+    text: str  # lo que se embebe y se indexa en BM25/FTS
+    embedding: list[float] | None = None
+    embedding_model: str = ""
+    embedding_dim: int = 0
+    index_version: str = ""
+    content_sha: str = ""
+
+
+class InformalChunk(ChunkBase):
+    """Tabla `informal`: problem_card, solution_step, figure, paper_section, theorem."""
+
+    corpus: Literal["informal"] = "informal"
+    parent_id: str | None = None
+    children_ids: list[str] = Field(default_factory=list)
+    order: int = 0
+    content_md: str = ""
+    context_summary: str = ""
+    page_start: int | None = None
+    page_end: int | None = None
+    bboxes: list[list[float]] = Field(default_factory=list)  # [page, x0, y0, x1, y1] normalizados
+    section_path: list[str] = Field(default_factory=list)
+    item_number: int | None = None
+    language: str = "es"
+    math_area: list[str] = Field(default_factory=list)
+    techniques: list[str] = Field(default_factory=list)
+    theorems_used: list[str] = Field(default_factory=list)
+    mathlib_candidates: list[str] = Field(default_factory=list)
+    difficulty: int | None = None
+    keywords: list[str] = Field(default_factory=list)
+    figure_ids: list[str] = Field(default_factory=list)
+    refs_to: list[str] = Field(default_factory=list)
+
+
+class MathlibChunk(ChunkBase):
+    """Tabla `mathlib`: una declaración por registro (§7.4)."""
+
+    corpus: Literal["mathlib"] = "mathlib"
+    unit_type: Literal["mathlib_decl"] = "mathlib_decl"
+    decl_name: str
+    decl_names_alt: list[str] = Field(default_factory=list)
+    module_path: str = ""
+    kind: str = ""
+    signature: str = ""
+    type: str = ""
+    value: str = ""
+    informal_name: str = ""
+    informal_description: str = ""
+    docstring: str = ""
+    dependencies: list[str] = Field(default_factory=list)
+    mathlib_tag: str = ""
+    lean_version: str = ""
+    docs_url: str = ""
+
+
+class Figure(BaseModel):
+    """§7.3 — tabla `figures`; también existe como InformalChunk(unit_type='figure')."""
+
+    figure_id: str
+    image_path: str
+    image_sha: str = ""
+    page: int
+    bbox: list[float]
+    detected_by: Literal["layout", "vector_cluster", "raster", "both"]
+    caption: str = ""
+    description: str = ""
+    labels: list[str] = Field(default_factory=list)
+    objects: list[str] = Field(default_factory=list)
+    relations: list[str] = Field(default_factory=list)
+    given_values: list[str] = Field(default_factory=list)
+    figure_type: Literal["geometric_diagram", "grid", "plot", "table_image", "other"] = "other"
+    linked_chunk_ids: list[str] = Field(default_factory=list)
+    description_model: str = ""
+    description_version: str = ""
+
+
+# ---------------------------------------------------------------------------
+# §7.5 — Citation
+# ---------------------------------------------------------------------------
+
+
+class RetrievalContext(BaseModel):
+    problem_id: str
+    subgoal_id: str = ""
+    attempt: int = 0
+    agent: str = ""
+    run_id: str = ""  # TRZ-1: si se da, el evento de traza va al archivo de esta corrida en vez de uno por búsqueda
+
+
+class CitationScores(BaseModel):
+    dense: float | None = None
+    sparse: float | None = None
+    fused: float | None = None
+    rerank: float | None = None
+
+
+class Citation(BaseModel):
+    citation_id: str
+    chunk_id: str
+    corpus: Corpus
+    unit_type: str
+    label: str
+    locator: dict = Field(default_factory=dict)
+    scores: CitationScores = Field(default_factory=CitationScores)
+    retrieved_for: RetrievalContext
+    used_in_proof: bool = False
+    used_in_sketch: bool = False
+    snippet: str = ""
+
+
+# ---------------------------------------------------------------------------
+# §7.6 — evento de traza JSONL (RNF-5)
+# ---------------------------------------------------------------------------
+
+
+class VersionsPin(BaseModel):
+    embedding_model: str = ""
+    reranker_model: str = ""
+    index_version: str = ""
+    mathlib_tag: str = ""
+    mathlib_table: str = ""  # MET-1: qué tabla sirve el corpus `mathlib` (`mathlib` muestra / `mathlib_full`)
+
+
+class HitRecord(BaseModel):
+    chunk_id: str
+    rank: int
+    scores: CitationScores = Field(default_factory=CitationScores)
+
+
+class TraceEvent(BaseModel):
+    run_id: str
+    problem_id: str
+    subgoal_id: str = ""
+    attempt: int = 0
+    agent: str = "retriever"
+    ts: str = Field(default_factory=lambda: datetime.now(timezone.utc).isoformat())
+    latency_ms: float = 0.0
+    llm_calls: int = 0  # el retriever SIEMPRE reporta 0 (RNF-3, §6.3 del plan)
+    tokens: int = 0
+    request: dict = Field(default_factory=dict)
+    n_candidates: int = 0
+    hits: list[HitRecord] = Field(default_factory=list)
+    versions: VersionsPin = Field(default_factory=VersionsPin)
+
+
+# ---------------------------------------------------------------------------
+# §8.1/§8.2 — contratos del recuperador
+# ---------------------------------------------------------------------------
+
+
+class RetrievalFilters(BaseModel):
+    math_area: list[str] = Field(default_factory=list)
+    doc_ids: list[str] = Field(default_factory=list)
+    unit_types: list[str] = Field(default_factory=list)
+    kinds: list[str] = Field(default_factory=list)
+
+
+class RetrievalRequest(BaseModel):
+    queries: list[str] = Field(min_length=1, max_length=4)
+    rerank_against: str | None = None
+    mode: QueryMode = "nl"
+    corpora: list[Corpus] = Field(default_factory=lambda: ["mathlib"])
+    k: int = 8
+    n_candidates: int = 50
+    filters: RetrievalFilters = Field(default_factory=RetrievalFilters)
+    rerank: bool = True
+    include_figures: bool = True
+    context: RetrievalContext
+
+
+class Hit(BaseModel):
+    chunk_id: str
+    corpus: Corpus
+    unit_type: str
+    rank: int
+    text: str
+    content_md: str = ""
+    metadata: dict = Field(default_factory=dict)
+    figures: list[dict] = Field(default_factory=list)
+    citation: Citation
+
+
+class RetrievalTrace(BaseModel):
+    latency_ms: float = 0.0
+    n_candidates: int = 0
+    versions: VersionsPin = Field(default_factory=VersionsPin)
+
+
+class RetrievalResult(BaseModel):
+    hits: list[Hit] = Field(default_factory=list)
+    citations: list[Citation] = Field(default_factory=list)
+    trace: RetrievalTrace = Field(default_factory=RetrievalTrace)