| --- |
| 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`. |
|
|
