MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

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.

Some computer programs can check mathematical proofs line by line, helping make mathematics more reliable and reproducible. However, writing proofs for these systems is still frustratingly difficult. Often the obstacle is not a deep theorem, but a tiny “obvious” step that human mathematicians use without thinking, yet that has not been written down in the system’s library. Our work introduces MathlibLemma, an AI pipeline that looks for these missing background facts in Mathlib, the main mathematical library for the Lean proof assistant. The pipeline proposes useful candidate lemmas, repairs them until Lean can understand them, and then tries to prove them automatically. Successful results are checked by Lean, so they become verified pieces of mathematics rather than just AI guesses. MathlibLemma produced 1,506 verified proofs and a benchmark of 4,028 challenging statements for measuring future AI systems. A small curated set of generated lemmas has already been accepted into Mathlib. Our results suggest that AI can do more than solve isolated math problems: it can help build the shared formal libraries that make rigorous mathematics easier to write, check, and reuse.