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