MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

TL;DR

This work introduces MathlibLemma, the first LLM-driven multi-agent system designed to proactively discover and formalize folklore lemmas missing from Mathlib, thereby closing the last-mile gap in formal mathematics. The framework decomposes the task into four stages—Discovery, Judge, Formalizer, and Prover—producing a verified library and a large-scale benchmark of $4{,}028$ Lean statements, of which $1{,}812$ have been formally proven. A rigorous human audit finds $78{\%}$ of sampled residuals provable, demonstrating a strong alignment with mathematical truth and exposing model limitations in deep structural reasoning. The study also reports substantial practical impact, with several generated lemmas upstreamed into Mathlib, highlighting the practicality of AI-assisted, self-evolving formal ecosystems.

Abstract

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, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas. This framework constitutes our primary contribution, proactively mining the missing connective tissue of mathematics. Its efficacy is demonstrated by the production of a verified library of folklore lemmas, a subset of which has already been formally merged into the latest build of Mathlib, thereby validating the system's real-world utility and alignment with expert standards. Leveraging this pipeline, we further construct the MathlibLemma benchmark, a suite of 4,028 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 establishes a constructive methodology for the self-evolution of formal mathematical libraries.

Figures (5)

• Figure 1: Overview of MathlibLemma. A multi-agent pipeline where the Discovery Agent mines candidates from Mathlib seeds, followed by semantic filtering (Judge), syntactic repair (Formalizer), and proof generation (Prover), yielding a verified library and benchmark.
• Figure 2: MathlibLemma taxonomy and composition. The benchmark is partitioned into three distinct domains (inner ring): Foundational, Applied, and Abstract. The outer ring shows topic areas used to source seed contexts, with representative examples in parentheses.
• Figure 3: Performance on Foundational Domain. This domain comprises standard mathematical structures (e.g., lists, real analysis basics) that are well-represented in the training data. Here, "GPT" denotes GPT-5.1, "GPT-Reasoning" denotes GPT-5.1 with low reasoning, and "DS" denotes DeepSeek-R1-Distill-Qwen (32B and 70B variants). Goedel-Prover shows a strong baseline, with cumulative success (Success@2) nearly 30%. The significant contribution of "0-trial" (One-shot) success indicates that frontier models have internalized many foundational definitions, and general-purpose open-weight models (e.g., DeepSeek) struggle with basic formalization, with scaling from 32B to 70B yielding no performance gain.
• Figure 4: Performance on Applied Domain. This domain includes fields like probability and information theory, where intuitive concepts often require complex type-class constraints. We find that all models achieve lower success rates on this domain than on the Foundational and Abstract domains (Figure \ref{['fig:foundational']} and \ref{['fig:abstract']}), but models with stronger reasoning—most notably GPT-5.1 (low reasoning)—perform comparatively better.
• Figure 5: Performance on Abstract Domain. This domain covers category theory and differential geometry. Compared to the Foundational and Applied domains (Figure \ref{['fig:foundational']} and \ref{['fig:applied']}), GPT-5.1 and GPT-5.1 (low reasoning) achieve higher success rates, while specialized models like Goedel and open-weight models like DeepSeek show a marked drop in performance.