# LemmaHead: RAG Assisted Proof Generation Using Large Language Models

arXiv: https://arxiv.org/abs/2501.15797 · HTML: https://mlsanity.com/paper/2501.15797/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 6 references that are in the map.
- First posted on arXiv 27 Jan 2025.

## Builds on (most cited first, 5 of 5)

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Metacognitive Capabilities of LLMs: An Exploration in Mathematical Problem Solving](https://mlsanity.com/paper/2405.12205/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically](https://mlsanity.com/paper/2411.01829/) (2024)

## Built on by (most cited first, 3 of 3)

- [A Survey on Large Language Models for Mathematical Reasoning](https://mlsanity.com/paper/2506.08446/) (2025)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)

## Abstract (arXiv)

Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consists of fine-tuning the model on written mathematical content such as academic publications and textbooks, so that the model can learn to emulate the style of mathematical writing. In this project, we explore the effectiveness of using retrieval augmented generation (RAG) to address gaps in the mathematical reasoning of LLMs. We develop LemmaHead, a RAG knowledge base that supplements queries to the model with relevant mathematical context, with particular focus on context from published textbooks. To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving via generating proofs to a given mathematical claim in the Lean formal language.