Technical Summary: MATHLIBLEMMA

1. Problem Statement

The formal mathematics ecosystem, particularly Lean and its library Mathlib, faces a "last-mile" barrier that hinders its adoption as an everyday tool comparable to LaTeX or Maple. While large language models (LLMs) have advanced automated theorem proving, a persistent bottleneck remains: the absence of "folklore lemmas." These are intermediate facts that working mathematicians routinely use and consider obvious (often learned implicitly from textbooks or practice) but are not explicitly present in formal libraries in a reusable form.

When such lemmas are missing, formalization stalls on trivial but necessary steps, and LLM-based provers are forced to reconstruct results from scratch rather than invoking them. This expands the search space, consumes context tokens, and increases the likelihood of hallucination and failure. Current evaluations often focus on fixed, Olympiad-level problem sets (e.g., MiniF2F) which are reaching performance saturation, failing to address the structural need for dense, reusable library expansion.

2. Methodology: The MATHLIBLEMMA Pipeline

The authors introduce MATHLIBLEMMA, a modular, LLM-based pipeline designed to proactively mine, formalize, and prove these missing folklore lemmas. The system operates through four distinct stages to factorize failure modes (semantic hallucination, syntactic errors, and proof search failure) into orthogonal components:

1. Discovery Module (Context-Aware Generation):

   • Input: Existing Mathlib source files (seeds).
   • Process: An LLM is prompted to brainstorm plausible missing lemmas based on the seed context, focusing on structural gaps and cross-topic interactions.
   • Output: Raw candidate statements in Lean code containing sorry placeholders, without attempting proofs.

2. Judge Module (Semantic Filtering):

   • Process: An LLM acts as a judge to assess the mathematical correctness of the raw candidates, explicitly ignoring Lean syntax well-formedness.
   • Goal: To filter out mathematically false or nonsensical statements before expensive kernel checking or proof search.
   • Output: A binary verdict (correct/wrong); only "correct" candidates proceed.

3. Formalizer Module (Kernel-Guided Repair):

   • Process: The system interacts with a Lean server (Kimina Lean server) to type-check the semantically filtered statements.
   • Loop: If errors occur, an LLM iteratively repairs syntax, namespaces, and implicit arguments based on compiler diagnostics. The loop terminates when the statement compiles without error-level diagnostics or a maximum trial count is reached.
   • Output: Type-checked Lean statements (still with sorry).

4. Prover Module (Proof Search & Verification):

   • Process: A prover LLM attempts to generate a full proof for the type-checked statement.
   • Verification: Successful attempts must pass two checks:
     1. Lean Kernel Check: The file must elaborate without errors.
     2. Proof-Bypass Screen: The generated code is stripped of comments and checked to ensure it contains no incomplete placeholders (sorry, admit, sorryAx) and no model-introduced top-level declarations that add new assumptions (axiom, constant, opaque).
   • Loop: Failed proofs trigger a generate-verify-repair loop (up to 2 repair rounds).

3. Key Contributions

A. The MATHLIBLEMMA Benchmark

The pipeline generated a benchmark suite of 4,028 non-trivial, type-checked Lean statements spanning three domains:

• Foundational: Real analysis, discrete structures, basic probability.
• Applied: Advanced probability (martingales), information theory, convex analysis.
• Abstract: Category theory, algebraic topology, differential geometry.

Unlike previous benchmarks, these are novelly discovered conjectures without pre-existing ground-truth proofs. The authors performed a human provability audit on a seed-stratified sample of model-unsolved residuals, finding that 78% were mathematically sound and provable by experts, indicating that many failures are due to current prover limitations rather than false statements.

B. A Verified Folklore Library

The pipeline produced a repository of 1,506 Lean-checked proofs that passed the proof-bypass screen. This serves as a reusable asset for the community.

• Upstreaming Validation: A small pilot effort submitted six curated lemmas to Mathlib. Three were merged, providing external evidence that selected outputs can meet expert library standards. The merged examples include a monotonicity lemma for the Grönwall bound, a kernel compatibility lemma in measure theory, and an almost-everywhere congruence lemma for central moments in probability.

C. Evaluation of State-of-the-Art Models

The benchmark was used to evaluate various models (GPT-5.1, DeepSeek-R1 variants, Goedel-Prover, Kimina-Prover, Qwen3) under a closed-book constraint (no external retrieval).

• Results: The union of all models proved 37.39% of the lemmas, while the best individual model (Goedel-Prover) proved 19.39%.
• Specialist vs. Generalist: Goedel-Prover excelled in Foundational domains (27.42%) but struggled in Abstract domains (8.24%), whereas GPT-Reasoning showed more consistent performance across domains.
• Diversity: The significant gap between the best single model and the union performance suggests that future systems should prioritize ensembling diverse architectures.

4. Significance and Claims

The paper claims that MATHLIBLEMMA represents a shift in the role of LLMs from passive consumers of formal libraries to active contributors in their expansion.

• Addressing the Last-Mile Gap: By proactively mining the "connective tissue" of mathematics, the work addresses the structural barrier of missing folklore lemmas that limits the usability of proof assistants.
• Constructive Methodology: The framework provides a constructive methodology for automated library expansion, validated by both the successful upstreaming of proofs into Mathlib and the high validity rate of human-audited residuals.
• Benchmarking Shift: It moves the evaluation focus from solving isolated, hard puzzles (Olympiad problems) to the foundational task of formalizing the vast quantity of routine background facts that human mathematicians take for granted.

The authors acknowledge limitations, including reliance on syntactic uniqueness for novelty filtering (potentially missing semantic duplicates), the lack of semantic-consistency checks in the repair loop, and the need for human curation regarding naming, placement, and generality before final integration into Mathlib. They position the work as a step toward AI-assisted expansion of formal mathematical libraries rather than a fully autonomous solution.