---
license: apache-2.0
tags: [lean4, mathlib, retrieval, rag, theorem-proving, olympiad, multi-agent]
datasets: [CamiloS1111/ragsolver-index]
---
# 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`](https://huggingface.co/datasets/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](https://github.com/camiloAndres11/RagSolver)):
`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`.