MathlibLemma

Official repository for the paper
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
Xinyu Liu, Zixuan Xie, Amir Moeini, Claire Chen, Shuze Daniel Liu, Yu Meng, Aidong Zhang, Shangtong Zhang

This repository contains MathlibLemma, a dataset of synthesized "folklore" lemmas that bridge the gap between high-level intuition and formal verification in Lean 4. It serves both as a library of verified theorems and a benchmark for evaluating the formal reasoning capabilities of LLMs.

📂 Repository Structure

The repository is organized into two main components:

• benchmark/: Contains the 4,028 type-checked statements (without proofs). These serve as the test set for auto-formalization and theorem proving tasks.
• lemma/: Contains the 1,812 formally verified theorems (with complete proofs generated by our pipeline).

Each component is categorized into three domains based on the complexity and abstraction level of the mathematics:

Directory	Description
foundational/	This domain covers the “bread and butter” of formalized mathematics: real analysis, discrete structures (e.g., sets, matrices), basic probability, and others.
applied/	This domain includes domains such as advanced probability (martingales), information theory, and convex analysis.
abstract/	This domain spans abstract fields including category theory, algebraic topology, and differential geometry.

🚀 Usage

This is a standard Lean 4 project. To build the project and verify the lemmas:

1. Install Lean 4: Follow the instructions at leanprover-community/lean4.
2. Clone the repository:

   git clone https://github.com/Sequential-Intelligence-Lab/MathlibLemma.git
   cd MathlibLemma

3. Get dependencies:

   lake exe cache get

4. Build:

   lake build

🏆 Merged Contributions to Mathlib

A key contribution of this project is the discovery of missing lemmas that have been accepted into the official Mathlib library. Below are the representative merged Pull Requests:

• Mathlib4 PR #32170

  • Adds gronwallBound_mono: gronwallBound is monotone non-decreasing in time x (given non-negative parameters δ, ε, K).

• Mathlib4 PR #32167

  • Adds Kernel.restrict_const: restricting a constant kernel to a measurable set commutes with restricting the underlying measure.

• Mathlib4 PR #31985

  • Adds centralMoment_congr_ae: central moments agree for a.e.-equal random variables.

Contributed by Sequential Intelligence Lab (SIL), University of Virginia.

📖 Citation

If you find this repository useful, please cite our paper.

@article{liu2026mathliblemma,
      title={MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics}, 
      author={Xinyu Liu and Zixuan Xie and Amir Moeini and Claire Chen and Shuze Daniel Liu and Yu Meng and Aidong Zhang and Shangtong Zhang},
      year={2026},
      journal={arXiv preprint arXiv:2602.02561}
}

📄 License

This project is licensed under the Apache License 2.0; see LICENSE.