用AI自动发现并证明数学中被忽略的常识性定理，提升形式化数学库可用性。
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
- 基于LLM的流水线主动挖掘数学中的隐含定理并形式化验证
- 生成1506个通过验证的可复用定理，4028个测试题覆盖多个数学领域
- 成果已合并至Mathlib，适合形式化数学与AI辅助证明研究者
尽管大型语言模型（LLMs）助力Lean和Mathlib在形式化数学推理中取得显著进展，但大量数学界公认的常识性定理仍未被纳入形式化库，成为限制Lean作为日常数学工具（如LaTeX或Maple）普及的关键障碍。为此，本文提出MathlibLemma，一种模块化的基于LLM的自动化民间定理挖掘流程：发现、形式化并证明数学家常默认但未明文记录的中间结论。该流程主动补全数学的“连接组织”。产出包含1,506个经过Lean验证且通过证明绕过检测的定理；其中一小部分精选结果已正式合并至Mathlib，提供了输出质量符合专家标准的外部证据。进一步地，基于该流程构建了MathlibLemma基准，涵盖4,028个非平凡、类型检查通过的Lean语句，覆盖广泛数学领域。本工作将LLM角色从被动使用者转变为积极贡献者，推动形式化数学库的智能扩展。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。