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
Proceedings of the 43rd International Conference on Machine Learning, PMLR 306:79178-79197, 2026.

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, 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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v306-liu26ez, title = {{M}athlib{L}emma: Folklore Lemma Generation and Benchmark for Formal Mathematics}, author = {Liu, Xinyu and Xie, Zixuan and Moeini, Amir and Chen, Claire and Liu, Shuze Daniel and Meng, Yu and Zhang, Aidong and Zhang, Shangtong}, booktitle = {Proceedings of the 43rd International Conference on Machine Learning}, pages = {79178--79197}, year = {2026}, editor = {Zhang, Tong and Dudik, Miroslav and Jaggi, Martin and Agarwal, Alekh and Li, Sharon and Schuurmans, Dale and Zhu, Jerry and Berkenkamp, Felix and Dong, Hanze and Bietti, Alberto}, volume = {306}, series = {Proceedings of Machine Learning Research}, month = {06--11 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v306/main/assets/liu26ez/liu26ez.pdf}, url = {https://proceedings.mlr.press/v306/liu26ez.html}, 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, 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.} }
Endnote
%0 Conference Paper %T MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics %A Xinyu Liu %A Zixuan Xie %A Amir Moeini %A Claire Chen %A Shuze Daniel Liu %A Yu Meng %A Aidong Zhang %A Shangtong Zhang %B Proceedings of the 43rd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2026 %E Tong Zhang %E Miroslav Dudik %E Martin Jaggi %E Alekh Agarwal %E Sharon Li %E Dale Schuurmans %E Jerry Zhu %E Felix Berkenkamp %E Hanze Dong %E Alberto Bietti %F pmlr-v306-liu26ez %I PMLR %P 79178--79197 %U https://proceedings.mlr.press/v306/liu26ez.html %V 306 %X 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.
APA
Liu, X., Xie, Z., Moeini, A., Chen, C., Liu, S.D., Meng, Y., Zhang, A. & Zhang, S.. (2026). MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics. Proceedings of the 43rd International Conference on Machine Learning, in Proceedings of Machine Learning Research 306:79178-79197 Available from https://proceedings.mlr.press/v306/liu26ez.html.

Related Material