Upload folder using huggingface_hub

configs/agents.yaml

@@ -0,0 +1,250 @@
+# Fase 4 — grafo de agentes (docs/PLAN_RAG.md Fase 4; propuesta §6.1-6.3, §8.2).
+prompt_version: "3"   # 2: replan con memoria (DES-1), esqueleto + CLOSE + FILL; 3: prueba estructurada en `have` (el sistema la parte en goals)
+
+k_max: 3          # intentos GENERATE->FORMALIZE->VERIFY por problema ("sin Crítico" = 1)
+max_replans: 1
+llm_budget: 20    # RNF-3: llamadas LLM por problema; al agotarse -> FAIL
+
+retrieval:
+  k_mathlib: 8
+  k_informal: 3
+  n_candidates: 50
+  rerank: false   # el cross-encoder son 2.4 GB más de RAM; en la muestra de 40 consultas sumó +2.5 puntos de recall (docs/DECISIONS.md #40)
+
+lean:
+  # backend `repl` (lean-interact): `import Mathlib` una vez por corrida (~3-5 min) y ~0.3 s
+  # por teorema; `lake`: un proceso por verificación (~3 min c/u), sin estado.
+  backend: repl
+  imports: ["Mathlib", "Aesop"]   # cabecera estándar de miniF2F
+  timeout_s: 600
+  max_heartbeats: 400000
+
+# Flujo por goal (docs/PLAN_MEJORA_RAG.md Fases 2-4): el Autoformalizador escribe un esqueleto
+# `have … := by sorry`; cada `sorry` es un goal de Lean que se cierra con la batería CLOSE (0 LLM, con
+# las premisas recuperadas para ESE goal) y sólo los que quedan abiertos van al LLM (FILL).
+# false = flujo anterior (prueba entera de una vez, recuperación NL por subobjetivo) — config `rag_nl`.
+goal_mode: true
+close:
+  k_premises: 16     # premisas por goal (canal A: prior de competición filtrado por el goal)
+  dense_channel: false   # canal C (índice denso con el goal): recall@16 0.028 y hunde la fusión (DECISIONS #98)
+  timeout_s: 150     # por táctica (ProofStep); `try?` llega a 76 s en goals difíciles (cada sub-táctica con sus heartbeats)
+  # En orden; gana la primera que cierra el goal. `rag`: con premisas recuperadas; `plain`: lo que
+  # corre sin RAG (`no_rag`, `baseline_auto`; null = se omite). Medido en docs/PLAN_MEJORA_RAG.md §2.3.
+  tactics:
+    - {rag: "grind +lax [{premises}]", plain: "grind"}
+    - {rag: "nlinarith [{hints}]", plain: "nlinarith"}
+    - {rag: "grind +suggestions", plain: null}   # canal B: selección nativa de Lean (Sine Qua Non)
+    - {rag: "try?", plain: "try?"}
+
+# Demostrador especializado local (docs/PLAN_REDISENO_PROVER.md): Goedel-Prover-V2-8B en la GPU vía
+# llama-server (puerto 8082). Etapa 0: k_root muestras sobre el teorema completo (0 API); en CLOSE, los
+# goals que la batería no cierra se le piden como lemas (k_goal) antes de FILL. `rag_names`: en la
+# autocorrección, el RAG sugiere nombres que existen en el Mathlib fijado para los identificadores desconocidos.
+prover:
+  enabled: true
+  k_root: 8
+  k_goal: 2
+  max_goals: 2       # goals por intento que se le piden al demostrador (cada muestra son minutos en la GPU)
+  max_tokens: 11500   # slot de 12 288 tokens en el servidor (Q6_K, 8 slots; la GPU satura en ~70 tok/s agregados)
+  temperature: 0.8
+  correction_rounds: 1
+  rag_names: true
+  # Respaldo por API: si el demostrador no resuelve, ¿corre el bucle de agentes (PLAN → … → CRITIQUE)?
+  # Apagado: en eval-v3 costó US$0.06 en los 9 problemas no resueltos y no resolvió ninguno. Sin
+  # demostrador (servidor caído o `enabled: false`) los agentes corren siempre.
+  api_fallback: false
+  # DRAFT (Draft-Sketch-Prove): si la etapa 0 falla, el modelo de la API (`llm_draft`, con razonamiento)
+  # escribe plan + prueba informal y el demostrador recibe eso y `k_lemmas` lemas del RAG EN SU PROMPT
+  # (`k_draft` muestras). El prompt crece ~1-2k tokens: el servidor necesita slots de 16 384 (`--parallel 6`).
+  dsp: false
+  k_draft: 8         # 8 + 8 = 16 muestras; se compara con las primeras 16 de baseline_prover32 (mismas semillas, misma caché)
+  k_lemmas: 10
+
+llm_supports_vision: false   # imágenes de figuras en el prompt del Generador (sólo descripciones si false)
+# Self-consistency del Generador (propuesta §6.3): n bocetos y se elige el "medoide" (el más parecido
+# a los demás por solapamiento de tokens); cuesta n llamadas por intento. 1 = apagado (presupuesto RNF-3).
+generator_samples: 1
+sketch_max_tokens: 40000   # SKETCH (texto + razonamiento): con los 16 000 de `llm_draft`, 32 de 38 llamadas de eval-v4 se cortaron razonando, sin bloque Lean (#128)
+
+# Configuraciones de ablación (propuesta §8.2). Cada una sobreescribe claves de arriba.
+configs:
+  full: {}
+  no_rag: {rag: false}               # misma batería CLOSE y mismo demostrador, sin premisas recuperadas, ejemplares ni sugerencias de nombres
+  no_critic: {k_max: 1}
+  rag_nl: {goal_mode: false}         # el flujo de eval-v1: recuperación NL por subobjetivo y prueba entera
+  baseline_auto: {mode: baseline_auto}   # 0 LLM: sólo la batería CLOSE (sin premisas) sobre el goal raíz
+  baseline_prover: {mode: baseline_prover}   # 0 API: sólo el demostrador local (k_root + autocorrección con errores de Lean, sin RAG)
+  baseline_prover32: {mode: baseline_prover, prover: {k_root: 32}}   # control de DRAFT: mismo presupuesto de muestras (8 + 24) sin plan ni lemas
+  dsp: {prover: {dsp: true}}         # etapa 0 + DRAFT (plan y prueba informal de la API + lemas del RAG en el prompt del demostrador)
+  # Para data/eval/problems/pdf_set.jsonl (sale del PDF del corpus informal): sin ejemplares informales, que
+  # traerían la solución del propio problema. Control: baseline_prover16 (mismas 8 + 8 muestras).
+  baseline_prover16: {mode: baseline_prover, prover: {k_root: 16}}
+  dsp8: {prover: {dsp: true}, corpora: ["mathlib"]}
+  # REPAIR (0 API): la prueba fallida del demostrador con menos errores se parte en sus `have`; sus propios bloques,
+  # la batería y el demostrador sobre el lema corto (4 pasos × 4 muestras) cierran los pasos que fallan
+  repair: {prover: {repair: 2, max_goals: 4, k_goal: 4}}
+  # SKETCH: además, el modelo con razonamiento (`llm_draft`) escribe el esqueleto Lean en pasos `have … := by sorry`
+  # (texto, no JSON) y CLOSE + demostrador cierran cada paso; 2 rondas (la 2.ª ve los pasos que quedaron abiertos)
+  sketch: {prover: {repair: 2, sketch: 2, max_goals: 4, k_goal: 4}}
+  # RAG de pruebas (rag/proofs.py): las pruebas verificadas de los 3 problemas más parecidos de Lean Workbook
+  # (embeddings), primero tal cual y luego como ejemplos en el prompt del demostrador (8 + 8; control: baseline_prover16)
+  rag_proofs: {prover: {examples: 3, k_examples: 8, max_sim: 0.95}}
+  baseline_a: {mode: baseline_a}   # LLM único: prueba Lean directa, sin agentes
+  baseline_b: {mode: baseline_b}   # LLM único: CoT en lenguaje natural, sin verificación
+
+prompts:
+  system: |
+    You are part of a multi-agent system that solves olympiad-level mathematics problems and certifies
+    the solutions with Lean 4 + Mathlib (tag v4.28.0-rc1). Be precise and terse. Only reference Mathlib
+    declarations that you are sure exist or that appear in the provided context. Answer in English.
+  planner: |
+    Decompose the problem into an ordered list of 1-5 subgoals (chain-of-thought), each one a claim that
+    a proof would establish on the way to the final statement. For each subgoal give: a natural-language
+    statement, a Lean-flavoured formal hint (informal, e.g. "n^2 % 4 = 0 ∨ n^2 % 4 = 1"), 2-3 short search
+    queries to find Mathlib lemmas for it (name the objects and the property: "gcd commutative", "sum of
+    consecutive integers", "prime divides product"), and its math area
+    (algebra | number_theory | combinatorics | geometry | inequalities | analysis).
+
+    ## Problem (natural language)
+    {informal}
+
+    ## Formal statement (Lean 4)
+    {formal}
+
+    ## Similar solved problems (for analogy; cite ids if useful)
+    {exemplars}
+
+    ## Replan feedback (why the previous plan failed and what is already proved; "(none)" on the first plan)
+    {feedback}
+  generator: |
+    Write a complete proof sketch in natural language for the problem, following the plan. Use the
+    retrieved Mathlib lemmas when they apply and say which ones you use by their ids (M1, M2, ...).
+    Use the worked examples only for the idea (ids I1, I2, ...). Be explicit about every algebraic step
+    so that a formalizer can turn each step into Lean tactics. The `sketch` field must contain that whole
+    proof written out, not a remark about which lemmas you use. If previous feedback is given, fix exactly
+    what it says.
+
+    ## Problem
+    {informal}
+
+    ## Formal statement (Lean 4)
+    {formal}
+
+    ## Plan
+    {plan}
+
+    ## Retrieved Mathlib lemmas
+    {lemmas}
+
+    ## Similar solved problems
+    {exemplars}
+
+    ## Feedback from the previous attempt
+    {feedback}
+  formalizer: |
+    Translate the proof sketch into Lean 4 tactics for the theorem below. Output ONLY the tactic block
+    that goes after `:= by` (do not repeat the theorem statement, do not add imports, do not use `sorry`,
+    `admit` or `axiom`). Prefer robust tactics (`nlinarith`, `linarith`, `norm_num`, `omega`, `simp`,
+    `ring_nf`, `positivity`, `decide`, `interval_cases`, `rcases`, `constructor`, `refine`) and the exact
+    names and signatures of the retrieved lemmas. Intermediate claims go in `have` steps. Mathlib is
+    imported (`import Mathlib`). If a previous Lean error is given, repair the proof accordingly.
+
+    ## Theorem
+    {formal}
+
+    ## Proof sketch
+    {sketch}
+
+    ## Retrieved Mathlib lemmas (exact names and signatures)
+    {lemmas}
+
+    ## Lean error from the previous attempt
+    {lean_error}
+  formalizer_skeleton: |
+    Translate the proof sketch into a Lean 4 proof SKELETON for the theorem below. Output ONLY the tactic
+    block that goes after `:= by` (do not repeat the theorem statement, do not add imports). Write each
+    intermediate claim of the sketch as its own top-level step `have hᵢ : <claim> := by <tactics>`, then
+    close the main goal from the `have`s. Keep each claim short; each step is checked by Lean on its own, and
+    a step that fails is retried with automation (`nlinarith`, `grind`, `omega`) and retrieved lemmas, so a
+    short claim with a simple proof is better than a long one. If you do not know how to prove a step, write
+    `sorry` as its proof (only as the whole proof of a `have`, never `<;> sorry` or `all_goals sorry`).
+    Mathlib is imported.
+
+    ## Theorem
+    {formal}
+
+    ## Proof sketch
+    {sketch}
+
+    ## Retrieved Mathlib lemmas (exact names and signatures)
+    {lemmas}
+
+    ## Claims already proved in previous attempts (keep these `have` statements verbatim; their proofs are reused)
+    {proved}
+
+    ## Lean error from the previous attempt
+    {lean_error}
+  sketcher: |
+    Write a Lean 4 proof skeleton (Mathlib, tag v4.28.0-rc1) for the theorem below. First work out the
+    mathematical proof. Then split it into small intermediate claims, each one a top-level
+    `have name : statement := by sorry` that is easy to prove on its own: one computation, one inequality,
+    one case, one induction. State general facts with ∀ (e.g. a closed form proved by induction) and derive
+    the specific statement from them. After the `have` steps, close the goal with tactics that use them
+    (`linarith`, `nlinarith [...]`, `omega`, `simp [...]`, `norm_num [...]`, `exact ...`). Keep every `have` at
+    the top level of the proof (not inside `cases` or `induction` branches). Output exactly one ```lean4 code
+    block with the complete theorem (same name and statement), without imports.
+    Informal statement:
+    {informal}
+    Lean statement:
+    {formal}
+    Feedback on your previous skeleton:
+    {feedback}
+  fill: |
+    Prove each open Lean 4 goal below. Each goal lists its hypotheses and, after `⊢`, its target. For each
+    goal output the tactic block that proves it completely: it replaces a `sorry` exactly at that goal. Use
+    the listed lemmas (exact names and signatures) when they help. Automation (grind, nlinarith, try?)
+    already failed on these goals; its last error is shown. Do not use `sorry`.
+
+    ## Theorem
+    {formal}
+
+    ## Open goals
+    {goals}
+  critic: |
+    The Lean 4 kernel rejected the proof. Classify the failure and decide the next action.
+    error_type: lean_syntax (parse/tactic misuse) | missing_lemma (unknown identifier or a needed lemma
+    not available) | misformalization (the sketch does not match the formal statement) | timeout |
+    planning (the plan itself is wrong) | unknown.
+    action: retry (fix generation/formalization with your feedback) | replan (the decomposition is wrong)
+    | abandon (no reasonable fix). List any identifiers that Lean reported as unknown. Give concrete,
+    actionable feedback (which step, what to change, which tactic).
+
+    ## Theorem
+    {formal}
+
+    ## Proof sketch
+    {sketch}
+
+    ## Lean proof attempted
+    {lean_code}
+
+    ## Lean errors
+    {lean_error}
+
+    ## History of attempts
+    {history}
+  baseline_a: |
+    Prove the following theorem in Lean 4 with Mathlib. Output ONLY the tactic block that goes after
+    `:= by` (no statement, no imports, no `sorry`).
+
+    ## Theorem
+    {formal}
+
+    ## Problem (natural language)
+    {informal}
+  baseline_b: |
+    Solve the following problem with a careful chain-of-thought proof in natural language. Then judge
+    honestly whether your proof is complete and correct (self_assessed_correct).
+
+    ## Problem
+    {informal}

configs/ingest.yaml

@@ -0,0 +1,74 @@
+# Configuración de ingesta. Sólo la sección `mathlib` se usa en Fase 1;
+# la sección `pdf` se completa en Fase 2 (docs/PLAN_RAG.md §6.2).
+
+mathlib:
+  raw_jsonl: "data/corpus/_raw/lsv2-mathlib-v4.28.0-rc1.jsonl"
+  out_jsonl: "data/corpus/mathlib.jsonl"
+  doc_id: "mathlib-v4.28.0-rc1"
+  docs_url_base: "https://leanprover-community.github.io/mathlib4_docs"
+  # Filtro Fase 1, tarea 3 (docs/PLAN_RAG.md): excluir ruido antes de embeber.
+  exclude_kinds: ["instance"]
+  exclude_module_prefixes: ["Mathlib.Tactic", "Mathlib.Deprecated"]
+  exclude_name_substrings: [".proof_", ".match_", "_aux"]
+  exclude_name_regex: '\.eq_(\d+|def)$'   # antes ".eq_" (subcadena) también borraba lemas reales
+
+pdf:
+  render_dpi: 200
+  # Calibrado con datos reales sobre problemas resueltos olimpiadas.pdf (docs/DECISIONS.md):
+  # filtra por tamaño mínimo del cluster (ambas dimensiones), no por cantidad de trazos.
+  vector_cluster_min_size_pt: 15.0
+  vector_cluster_min_overlap: 0.6
+  figure_crop_padding_pt: 10.0
+  # Regiones con >= N palabras de la capa de texto fuera de todo bloque de MinerU
+  # se transcriben con el VLM (Plan B acotado, docs/PLAN_RAG.md Fase 2).
+  gap_min_words: 4
+
+# Fase 2, tarea 6 — prompts fijos y versionados (docs/PLAN_RAG.md §6.2). Cambiar
+# `prompt_version` invalida la caché de data/parsed/<doc_id>/enrich/*.jsonl.
+enrich:
+  prompt_version: "1"
+  math_areas: [algebra, number_theory, combinatorics, geometry, inequalities, analysis, probability, logic, other]
+  techniques: [induction, pigeonhole, invariant, extremal_principle, parity, modular_arithmetic, vieta_jumping,
+               am_gm, cauchy_schwarz, rearrangement, telescoping, generating_functions, bijection,
+               double_counting, angle_chasing, similar_triangles, power_of_a_point, coordinates,
+               trigonometry, algebraic_manipulation, factorization, bounding, case_analysis, contradiction,
+               construction, recursion, symmetry, counting]
+  transcribe: |
+    Transcribe this fragment of a Spanish mathematics book exactly as it appears, as Markdown with LaTeX.
+    Rules: inline math in $...$; displayed equations in $$...$$ on their own lines; keep the original Spanish text;
+    if a line starts with an item number such as "77." keep it at the start of the line; underbraces, dots and
+    cancellations must be rendered in LaTeX. The crop may cut through a line of text at its top or bottom edge:
+    skip any line that is not completely visible. Output only the transcription, no commentary.
+  figure: |
+    You are annotating a figure from a Spanish olympiad problem book for a retrieval system. The figure has no
+    caption; use the problem (and solution, if given) as context to name the objects correctly.
+    Describe the attached figure in English for a reader who cannot see it. Be concrete: name every visible label,
+    every geometric object, the relations among them (tangency, perpendicularity, inscribed, midpoint, ...) and
+    every value written in the figure (angles, lengths, areas). Do not solve the problem.
+    figure_type: geometric_diagram | grid | plot | table_image | other.
+  formulas: |
+    The list below contains LaTeX extracted by OCR for the formulas on the attached page, in reading order
+    (displayed and inline formulas). Compare each item against the page image. Return the same number of items in
+    the same order. Keep the original LaTeX EXACTLY unless it misrepresents the mathematics in the image
+    (wrong or missing exponent, subscript, digit, symbol or operator; garbled text). Do not reformat, do not
+    change spacing, do not translate. The boundaries of each item are fixed: the plain text before and after a
+    formula is NOT part of it — never extend an item with neighbouring words, units or the next formula, even if
+    they belong together mathematically. If an item contains garbled non-math text, remove the garbage and keep
+    only the formula. Mark changed=true only for items you modified.
+  card: |
+    You are indexing a solved problem from a Spanish olympiad problem book for a retrieval system whose queries
+    are in English. Read the problem, its solution and the figure descriptions (if any) and return, in English:
+    - context_summary: 2-3 sentences situating this problem for retrieval: what is asked, the mathematical area,
+      the key idea of the solution and the main theorems or techniques used (Contextual Retrieval style).
+    - math_area: one or more of {math_areas}.
+    - techniques: from {techniques}; add others in snake_case only if none fits.
+    - theorems_used: standard English names of the theorems/results used (e.g. "inscribed angle theorem").
+    - difficulty: integer 1 (routine) to 5 (hard olympiad).
+    - keywords: 6-12 English keywords for lexical search (objects, concepts, named results).
+  split: |
+    The text below contains the solutions to problems {prev} and {n} of a Spanish problem book, concatenated,
+    because the OCR lost the "{n}." marker at the start of solution {n}. Using the two problem statements as a
+    guide, identify where solution {n} begins and return the first line of solution {n} copied VERBATIM from the
+    text (including any LaTeX, exactly as written). If solution {n} starts with a displayed equation, return the
+    LaTeX line inside the $$ block, never the "$$" delimiter itself. If solution {n} is not present, return an
+    empty string.

configs/retrieval.yaml

@@ -0,0 +1,23 @@
+# Fase 3 — servicio de recuperación (docs/PLAN_RAG.md §6.3, §8, Fase 4 tarea 7).
+# Los valores por consulta (k, n_candidates, rerank) los fija RetrievalRequest;
+# aquí van las plantillas por modo y los flags de ablación que aplica el orquestador.
+
+rrf_k: 60
+# 0 = sin límite. Evita que un módulo de Mathlib con muchas variantes del mismo
+# lema desplace a lemas de otros módulos (docs/PLAN_RAG.md §6.3, "opcional").
+max_per_module: 0
+
+# Instrucción de consulta de Qwen3-Embedding ("Instruct: ...\nQuery: ..."). Los
+# documentos se embebieron SIN instrucción, así que cambiar esto no obliga a
+# re-indexar. `nl` es la misma instrucción con la que se midió la Fase 1.
+query_instructions:
+  nl: "Given a mathematical query, retrieve relevant Mathlib declarations or worked problems."
+  formal: "Given a Lean 4 goal state or theorem statement, retrieve Mathlib declarations whose statements match it."
+  error: "Given a Lean 4 error message and goal, retrieve the Mathlib declaration it refers to or the closest alternatives."
+  exemplar: "Given a competition math problem, retrieve solved problems that use the same idea or technique."
+
+# Flags de ablación (docs/PLAN_RAG.md Fase 4, tarea 7; métrica 8.3 "contribución del RAG").
+# enabled=false -> RETRIEVE devuelve vacío y la traza lo registra igual.
+ablation:
+  enabled: true
+  corpora: [mathlib, informal]

configs/versions.yaml

@@ -0,0 +1,83 @@
+# Fuente única de verdad de versiones (RNF-2, docs/PLAN_RAG.md §0/§9).
+# Todo evento JSONL de traza (rag/schema.py:TraceEvent) copia este bloque.
+# ACTUALIZAR este archivo, no hardcodear versiones en el código.
+
+lean:
+  toolchain: "leanprover/lean4:v4.28.0-rc1"
+  mathlib_tag: "v4.28.0-rc1"
+  mathlib_commit: "5352afccd6866369be9de43f5b7ec47203555f44"
+
+embedding:
+  model: "Qwen/Qwen3-Embedding-0.6B"
+  dim: 1024
+  # subir a Qwen/Qwen3-Embedding-4B sólo si Fase 1 muestra ganancia medible en MathlibQR (ver §7 del plan)
+
+reranker:
+  model: "Qwen/Qwen3-Reranker-0.6B"
+
+parser:
+  name: "mineru"
+  version: "4.0.3"
+  tier: "standard"
+
+# Proveedor LLM/VLM (ragsolver.llm.LLM). `provider: gemini` usa GEMINI_API_KEY (.env);
+# `provider: openai_compatible` usa `base_url` + la variable de `api_key_env` — sirve para
+# OpenRouter (https://openrouter.ai/api/v1, OPENROUTER_API_KEY), OpenAI, Ollama o vLLM.
+# La cuota diaria del tier gratis de Gemini es por modelo (20 req/día en 3.5-flash, medido):
+# al agotarse se pasa al siguiente de `fallback_models`; cada resultado registra el modelo real.
+vlm_enrichment:
+  provider: "gemini"
+  model: "gemini-3.5-flash" # visión + JSON estructurado, verificado (docs/DECISIONS.md #13, #21)
+  fallback_models: ["gemini-3.5-flash-lite", "gemini-3.1-flash-lite", "gemma-4-31b-it", "gemma-4-26b-a4b-it", "gemini-3-flash-preview"]
+  temperature: 0.1
+  seed: 13
+  # provider: "openai_compatible"
+  # base_url: "https://openrouter.ai/api/v1"
+  # api_key_env: "OPENROUTER_API_KEY"
+  # model: "google/gemini-2.5-flash"
+
+llm: # agentes (Fase 4). Experimento principal: UN solo modelo para las 5 configuraciones (sin confundir modelo y configuración)
+  provider: "openai_compatible"        # OpenRouter (docs/DECISIONS.md #47); tope de gasto fijado en la cuenta
+  base_url: "https://openrouter.ai/api/v1"
+  api_key_env: "OPENROUTER_API_KEY"
+  model: "deepseek/deepseek-v4-flash-0731"   # $0.04/M in, $0.16/M out; JSON schema verificado
+  fallback_models: ["google/gemini-2.5-flash-lite"]
+  temperature: 0.2
+  seed: 13   # RNF-2; determinismo "best effort" del proveedor
+  max_tokens: 4000          # salida sin razonamiento; acota costo y latencia por llamada
+  reasoning_effort: "off"    # DeepSeek V4 Flash: planner 24 s sin razonar vs 76-92 s con low/medium (60×5 pares no cabrían en una noche)
+  timeout_s: 900
+  # OpenRouter: tope de precio por M tokens y, entre los que cumplen, el más barato (`sort: price`; #64 lo
+  # cambió de `sort: throughput` porque a igual tope de precio el más rápido no siempre es el más barato).
+  # `max_price` solo (sin `sort`) ya habría evitado el proveedor a $0.80/M de salida del #62.
+  # 2026-10-14 (#107): con {0.10, 0.20} sólo calificaba DeepInfra (StreamLake subió a $0.132/$0.396), saturado (429).
+  # Con {0.13, 0.30}: 8 proveedores; `sort: price` sigue usando primero DeepInfra ($0.06/$0.18) y pasa a los demás
+  # sólo cuando rechaza. eval-v1 corrió con el tope anterior.
+  provider_routing: {max_price: {prompt: 0.13, completion: 0.30}, sort: price}
+  # Alternativa gratuita usada en el desarrollo (cuota 20 req/día por modelo):
+  # provider: "gemini"; model: "gemini-3.5-flash"; fallback_models: ["gemini-3.5-flash-lite", "gemini-3.1-flash-lite", "gemma-4-31b-it", "gemma-4-26b-a4b-it", "gemini-3-flash-preview"]
+
+# Borrador de DRAFT (Draft-Sketch-Prove, configs/agents.yaml `prover.dsp`): el mismo modelo CON razonamiento.
+# Sin razonar, un planner tarda 24 s y con razonamiento 76-92 s (#50); aquí la latencia no importa (cada
+# muestra del demostrador son minutos de GPU) y el razonamiento es justo lo que este modelo aporta.
+# `max_tokens` incluye el razonamiento; 16 000 a ≤ US$0.30/M ≈ US$0.005 por llamada en el peor caso.
+llm_draft:
+  provider: "openai_compatible"
+  base_url: "https://openrouter.ai/api/v1"
+  api_key_env: "OPENROUTER_API_KEY"
+  model: "deepseek/deepseek-v4-flash-0731"
+  fallback_models: []
+  temperature: 0.2
+  seed: 13
+  max_tokens: 16000
+  reasoning_effort: "high"
+  timeout_s: 1800   # SKETCH pide hasta `sketch_max_tokens` (agents.yaml) de salida
+  provider_routing: {max_price: {prompt: 0.13, completion: 0.30}, sort: price}
+
+index:
+  backend: "lancedb"
+  version: "0.1.0" # semver del índice; incrementar si cambia embedding_model o esquema de chunk
+
+corpus_mathlib:
+  source: "FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl"
+  license: "Apache-2.0"