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