MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
本文介绍了 MathlibLemma，这是一个基于大语言模型的自动化流程，旨在发现并形式化缺失的“民间”引理以扩展 Lean Mathlib 库，同时建立一个包含 4000 多个已验证数学陈述的综合基准，以推动人工智能辅助的形式化数学发展。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图利用一个机器人助手，构建一座庞大且完美的数学知识图书馆。你拥有一座名为 Mathlib（为 Lean 证明助手构建）的巨型现有图书馆，它就像一本超级有条理的数学事实百科全书。
然而，这里有一个问题。虽然这座图书馆拥有那些宏大、著名的定理，但它却缺失了成千上万条微小、"显而易见"的事实，而这些正是人类数学家在日常思考中不加思索便使用的。这些被称为民间引理（folklore lemmas）。
不妨这样想：如果你正在写一部小说，你不需要解释"正方形有四条边"或"给一个数加零，它保持不变"。你只需假设每个人都懂。但对于机器人证明检查器而言，如果这些微小的事实没有被明确地写在图书馆中，它就会卡住。这就像试图建造一座房子，却发现自己忘了购买将屋顶固定在一起所需的特定类型钉子。房子（证明）在概念上是合理的，但由于缺失了一个微小、"显而易见"的部件，你无法完成施工。
问题："最后一公里"
该论文认为，这种缺失的"连接组织"构成了最后一公里障碍。它阻碍了数学家像使用文字处理器或计算器那样轻松地使用这些强大的计算机工具。即使人类知道证明过程，计算机也无法完成，因为它缺失了那些微小的中间步骤。
此外，当人工智能（大型语言模型）试图帮助编写这些证明时，往往会失败。为什么？因为如果人工智能在图书馆中找不到那个"显而易见"的事实，它就会试图从头开始发明整个证明。这就像要求某人在没有蓝图的情况下建造一座桥梁；他们可能会迷路、犯错，或者产生幻觉（编造内容），因为任务过于庞大。
解决方案：MATHLIBLEMMA
作者们创建了一个名为 MATHLIBLEMMA 的系统。可以将这个系统想象为一个四阶段工厂，旨在发现那些缺失的"显而易见"的事实，正确地将其书写下来，并证明其为真。
以下是该工厂逐步的工作方式：
探索者（发现模块）：
想象一位好奇的图书管理员，他阅读现有的图书馆并说："嘿，我们有很多关于三角形的事实，但我们没有关于将其上下翻转时会发生什么的规则。这很可能是真的，但它缺失了！"该模块利用人工智能，基于现有内容来构思这些缺失的事实。守门人（判断模块）：
探索者可能会犯错。它可能会提出一些听起来很酷但实际上在数学上是错误的建议（比如声称"所有数字都是偶数"）。守门人是第二个人工智能，它会审视这些建议并说："不，那是胡说八道"，或者"是的，这听起来是对的"。它在工厂浪费时间在垃圾上之前，将其过滤掉。编辑（形式化模块）：
即使一个想法在数学上是正确的，人工智能也可能以一种计算机无法理解的奇怪方式将其书写出来（比如语法错误的句子）。编辑会修正语法。它与计算机（Lean 服务器）对话，查看哪里出错了，获取错误信息，并要求人工智能进行修复，直到计算机说："好的，这个句子语法正确。"构建者（证明模块）：
现在事实已被正确书写，构建者尝试证明它。它试图构建逻辑论证。如果失败，它会收到错误信息，再次尝试并修正错误。如果成功，它将生成一个被计算机接受为 100% 真实的已验证证明。
他们的发现
团队运行了这个工厂，并产出了两项主要成果：
- 一个新的事实库： 他们发现并证明了 1,506 个这些缺失的"民间"事实。他们甚至选取了一小部分样本，成功将其添加到官方的 Mathlib 库中，证明了人工智能可以生成符合人类专家高标准的事实。
- 一个新的挑战（基准测试）： 他们创建了一个包含 4,028 个这些缺失事实的测试集，以观察不同的 AI 模型在发现和证明它们方面的表现如何。
结果：
- 当前的 AI 模型正在变得更好，但距离完美还有很长的路要走。最好的模型只能独立解决约 19% 的这些"显而易见"的事实。
- 然而，当你结合不同模型的优势（就像使用一个专家团队）时，它们可以解决约 37%。
- 至关重要的是，当人类专家审视那些 AI 未能解决的问题时，他们发现其中 78% 实际上是可解的且在数学上为真。这意味着 AI 的失败并非因为这些事实是虚假的；而是因为任务本身非常困难。
结语
这篇论文表明，我们可以利用人工智能不仅来消费现有的数学库，还可以主动扩展它们。通过自动化发现这些微小的缺失部分，我们正在帮助为形式化数学构建一个更完整、更可用、更可靠的基础。这就像填补地图上的空白，使得从数学概念到计算机验证证明的旅程变得顺畅而轻松。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。