# MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 24 of its 50 references that are in the map.
- First posted on arXiv 30 Jan 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [OpenAI GPT-5 System Card](https://mlsanity.com/paper/2601.03267/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically](https://mlsanity.com/paper/2411.01829/) (2024)
- [Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification](https://mlsanity.com/paper/2504.21230/) (2025)
- [ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis](https://mlsanity.com/paper/2501.18310/) (2025)
- [LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving](https://mlsanity.com/paper/2506.22005/) (2025)
- [Lemmanaid: Neuro-Symbolic Lemma Conjecturing](https://mlsanity.com/paper/2504.04942/) (2025)

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

- [Robust Data-Collection Policy Learning for Low-Variance Online Policy Evaluation](https://mlsanity.com/paper/2608.24146/) (2026)
- [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026)
- [Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery](https://mlsanity.com/paper/2606.08728/) (2026)
- [MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures](https://mlsanity.com/paper/2607.27709/) (2026)

## Abstract (arXiv)

While the ecosystem of Lean and Mathlib has enjoyed celebrated success in formal mathematical reasoning with the help of large language models (LLMs), the absence of many folklore lemmas in Mathlib remains a persistent barrier that limits Lean's usability as an everyday tool for mathematicians like LaTeX or Maple. To address this, we introduce MathlibLemma, a modular LLM-based pipeline for automated folklore-lemma mining: the discovery, formalization, and proving of reusable intermediate facts that mathematicians often take for granted but that are not always present in formal libraries. At its core, MathlibLemma proactively mines the missing connective tissue of mathematics. The pipeline produces a verified library of folklore-style lemmas, including 1,506 Lean-checked proofs that pass a proof-bypass screen; a small curated pilot subset has also been merged into Mathlib, providing external evidence that selected outputs can meet expert library standards. Leveraging this pipeline, we further construct the MathlibLemma benchmark, a suite of 4,028 non-trivial type-checked Lean statements spanning a broad range of mathematical domains. By transforming the role of LLMs from passive consumers to active contributors, this work takes a step toward AI-assisted expansion of formal mathematical libraries.