| cff-version: 1.2.0 |
| title: "RagSolver: a multi-agent system for olympiad-style problem solving with embeddings-based retrieval and Lean 4 verification" |
| message: "If you use this software, please cite it as below." |
| type: software |
| authors: |
| - given-names: "Camilo Andres" |
| family-names: "Niño Amaya" |
| affiliation: "Universidad Pedagógica y Tecnológica de Colombia (UPTC), Sogamoso" |
| - given-names: "Jose L." |
| family-names: "Salamanca" |
| affiliation: "Universidad Pedagógica y Tecnológica de Colombia (UPTC), Sogamoso" |
| version: 0.2.0 |
| date-released: "2026-10-21" |
| license: Apache-2.0 |
| repository-code: "https://github.com/camiloAndres11/RagSolver" |
| abstract: >- |
| Multi-agent pipeline (planner, retriever, generator, autoformalizer, verifier, critic) |
| orchestrated with LangGraph that solves competition mathematics problems and certifies |
| solutions with the Lean 4 kernel and Mathlib (v4.28.0-rc1). Retrieval-augmented generation |
| over the LeanSearch v2 informalized Mathlib corpus (LanceDB, hybrid dense + BM25) and over |
| a corpus of solved olympiad problems parsed from PDF (MinerU + VLM figure descriptions). A locally served |
| Lean prover (Goedel-Prover-V2-8B) is the first stage; the agents and retrieval act on what it leaves |
| unsolved (draft-sketch-prove, step-wise repair, Lean skeletons, retrieval of verified proofs of similar problems). |
| keywords: [Lean 4, Mathlib, retrieval-augmented generation, multi-agent systems, theorem proving, miniF2F, Goedel-Prover-V2] |
| references: |
| - type: dataset |
| title: "lsv2-mathlib-v4.28.0-rc1-jsonl (LeanSearch v2 corpus)" |
| authors: [{name: "FrenzyMath"}] |
| license: Apache-2.0 |
| - type: dataset |
| title: "miniF2F-v2" |
| authors: [{name: "roozbeh-yz"}] |
| license: Apache-2.0 |
| - type: software |
| title: "Goedel-Prover-V2-8B" |
| authors: [{name: "Goedel-LM"}] |
| license: Apache-2.0 |
| - type: dataset |
| title: "Lean-workbook-proofs" |
| authors: [{name: "Goedel-LM"}] |
| license: MIT |
|
|
