# LLM Library Learning Fails: A LEGO-Prover Case Study

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 22 references that are in the map.
- First posted on arXiv 3 Apr 2025.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [GAIA: a benchmark for General AI Assistants](https://mlsanity.com/paper/2311.12983/) (2023)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [ViperGPT: Visual Inference via Python Execution for Reasoning](https://mlsanity.com/paper/2303.08128/) (2023)
- [Large Language Models as Tool Makers](https://mlsanity.com/paper/2305.17126/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [AI Agents That Matter](https://mlsanity.com/paper/2407.01502/) (2024)
- [Is Self-Repair a Silver Bullet for Code Generation?](https://mlsanity.com/paper/2306.09896/) (2023)
- [CRAFT: Customizing LLMs by Creating and Retrieving from Specialized Toolsets](https://mlsanity.com/paper/2309.17428/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Tasks](https://mlsanity.com/paper/2401.12869/) (2024)
- [POSIX: A Prompt Sensitivity Index For Large Language Models](https://mlsanity.com/paper/2410.02185/) (2024)
- [LILO: Learning Interpretable Libraries by Compressing and Documenting Code](https://mlsanity.com/paper/2310.19791/) (2023)
- [DynaSaur: Large Language Agents Beyond Predefined Actions](https://mlsanity.com/paper/2411.01747/) (2024)
- [Sibyl: Simple yet Effective Agent Framework for Complex Real-world Reasoning](https://mlsanity.com/paper/2407.10718/) (2024)
- [Paraphrase Types Elicit Prompt Engineering Capabilities](https://mlsanity.com/paper/2406.19898/) (2024)
- [Library Learning Doesn't: The Curious Case of the Single-Use "Library"](https://mlsanity.com/paper/2410.20274/) (2024)

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

- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [A Compute-Matched Re-Evaluation of TroVE on MATH](https://mlsanity.com/paper/2507.22069/) (2025)
- [ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving](https://mlsanity.com/paper/2608.26334/) (2026)

## Abstract (arXiv)

Recent advancements in the coding, reasoning, and tool-using abilities of LLMs have spurred interest in library learning (i.e., online learning through the creation, storage, and retrieval of reusable and composable functions, knowledge, checklists, or lemmas). Such systems often promise improved task performance through the automatic creation of broadly applicable tools, as well as superior computational performance through the caching of reasoning (i.e., the storage of generated tools). However, we find strong reason to be skeptical. We perform a deep dive into one such system, LEGO-Prover, which purports to learn reusable lemmas for mathematical reasoning. We find no evidence of the direct reuse of learned lemmas, and find evidence against the soft reuse of learned lemmas (i.e., reuse by modifying relevant examples). Crucially, we find that LEGO-Prover does not in fact improve over the simple baseline of prompting the model - the improvements in task accuracy vanish once computational cost is accounted for. Our findings suggest that serious misconceptions exist as to the effectiveness of these techniques, that a serious re-examination of the state of LLM-based library learning is required, and that we require much stronger standards for evaluation including behavioural analysis and ensuring that an equal computational budget is used for baselines.