LeanDojo（精益道场）用LLMs实现定理证明

LeanDojo是一个开源平台，用于使用语言模型证明数学定理。

自动定理证明 （ATP） 是一项为形式逻辑中制定的定理生成证明的任务。它对形式化数学很有用，支持形式化验证，保证了高风险应用的正确性和安全性。

然而，由于其较大的搜索空间，ATP具有挑战性。因此，交互式定理证明（ITP）已成为一种替代方案。在ITP中，证明是由数学家与称为证明助手的软件工具交互生成的。

机器学习可以自动化这个过程，开辟一种证明定理的新方法。

更多技术信息：https://leandojo.org/

大型语言模型可以自动证明定理

大型语言模型与精益等证明助手相结合是此过程的候选者。然而，根据加州理工学院、英伟达大学、麻省理工学院、加州大学圣巴巴拉分校和德克萨斯大学奥斯汀分校的一组研究人员的说法，由于专有代码、数据和高计算要求，现有方法难以复制或发展。

为了解决这个问题，他们创建了LeanDojo，这是一个使用语言模型证明数学定理的开源平台。

的一组研究人员的说法，由于专有代码、数据和高计算要求，现有方法难以复制或发展。

LeanDojo为基于学习的定理证明提供了两个关键功能：数据提取和模型与广泛使用的证明助手Lean的编程交互。根据研究人员的说法，LeanDojo是第一个可以与Lean可靠交互的工具，这应该会显着减少证明错误。

LeanDojo还解决了定理证明中的一个关键瓶颈：前提选择。该团队通过ReProver（Retrieval-Augmented Prover）来证明这一点，ReProver是一种基于语言模型的证明器，它基于从Lean的数学库中检索到的一些前提生成证明策略。

根据该团队的说法，ReProver的性能优于其他一些方法，在LeanDojo基准测试以及两个现有数据集MiniF2F和ProofNet中证明了很大一部分定理。ReProver还可以证明目前在精益中没有证明的定理，使其成为扩展精益中现有数学库的有用工具。

到2026年，语言模型将共同创作数学？

该团队还发布了一个用LeanDojo构建的基准测试，其中包括来自Mathlib的近97，000个定理，以及GPT的插件。

数学家Terence Tao最近预测，到2026年，使用外部工具的语言模型可能会成为数学和其他科学领域值得信赖的合著者。LeanDojo和ReProver展示了这些工具的样子，现在为其他研究人员提供了改进的基础。

Summary 小结

• LeanDojo是一个开源平台，用于使用大型语言模型自动证明定理。
• 它由加州理工学院、英伟达大学、麻省理工学院、加州大学圣巴巴拉分校和德克萨斯大学奥斯汀分校开发，与精益证明助手交互，以实现高效的数据提取和交互。
• 通过ReProver，该团队提出了一个基于语言模型的证明器，该证明器已经证明了一些目前不存在证明的定理。
  github：https://github.com/lean-dojo