RagSolver — búsqueda de lemas de Mathlib (Lean 4, v4.28.0-rc1)

Recuperación híbrida (Qwen3-Embedding-0.6B + BM25, RRF) sobre 278 160 declaraciones de Mathlib informalizadas por LeanSearch v2, con citas (nombre, módulo, enlace a la documentación). Índice: CamiloS1111/ragsolver-index. El modo Resolver (agentes + verificación con el kernel de Lean) requiere una instalación local: docs/install.md. La demo (app.py, Gradio) se corre en local: bash scripts/demo_up.sh (docs/user_guide.md).

Este repositorio contiene el proyecto completo (GitHub): ragsolver/ (agentes, orquestador, recuperación, Lean), configs/, docs/ (arquitectura, instalación, guía de uso, interfaces, reproducción de cada ablación, informes de resultados e informe final), notebooks/, tests/, scripts/, pyproject.toml + uv.lock, LICENSE (Apache-2.0) y CITATION.cff.