Formal Language Knowledge Corpus for Retrieval Augmented Generation
On the map: Retrieval-augmented generation → Agentic RAG, agents and memory
Abstract (arXiv)
The integration of retrieval-augmented techniques with LLMs has shown promise in improving performance across various domains. However, their utility in tasks requiring advanced reasoning, such as generating and evaluating mathematical statements and proofs, remains underexplored. This study explores the use of Lean, a programming language for writing mathematical proofs, to populate the knowledge corpus used by RAG systems. We hope for this to lay the foundation to exploring different methods of using RAGs to improve the performance of LLMs in advanced logical reasoning tasks.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Placed in Agentic RAG, agents and memory, one of 15 directions in Retrieval-augmented generation. First posted on arXiv 21 Dec 2024.
Builds on
0 of 0 references.
No references here yet.
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2025LemmaHead: RAG Assisted Proof Generation Using Large Language Models
- 2025RAG+: Enhancing Retrieval-Augmented Generation with Application-Aware Reasoning
- 2025PIKE-RAG: sPecIalized KnowledgE and Rationale Augmented Generation
- 2024A Hybrid RAG System with Comprehensive Enhancement on Complex Reasoning
- 2025Automated Formalization via Conceptual Retrieval-Augmented LLMs
- 2025Synergizing RAG and Reasoning: A Systematic Review
- 2025Towards Agentic RAG with Deep Reasoning: A Survey of RAG-Reasoning Systems in LLMs
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Models