主要证据
- LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsS1 · 主要研究来源 · 论文 · 2023-06-27
- LeanDojo repositoryS1 · 主要研究来源 · 代码仓库
LeanDojo 建立可复现的 Lean 大模型定理证明环境
该项目从 Lean 仓库抽取证明状态、战术与前提信息，并提供可编程证明环境。ReProver 在生成战术前检索相关前提，直接处理大规模数学库中的前提选择问题。
发生了什么？
LeanDojo 公开了用于与 Lean 交互和训练定理证明器的工具与基准，并发布检索增强语言模型证明器 ReProver，在近十万个 mathlib 定理构成的基准上进行评测。
为什么重要？
LeanDojo 推动 Lean 定理证明成为更易进入的机器学习研究平台，并提供了后续形式数学 Agent 可复用的基础设施，避免重复搭建证明环境集成。
重要性说明：LeanDojo 将可编程 Lean 交互、证明数据抽取、大规模基准和开放的检索增强证明器整合起来，显著降低了学习式定理证明的复现门槛。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- ReProver 使用检索与语言模型生成选择前提并提出 Lean 战术，由证明助手判断生成的证明步骤是否有效。
- 人类贡献
- 研究者开发 Lean 数据抽取与交互工具、构建基准、训练检索器与生成器，并设计可复现的评测划分。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- leandojo, reprover, lean
- 机构
- caltech, nvidia
- 数学问题
- lean-theorem-proving
- 方法
- retrieval-augmented-generation, premise-selection, formal-theorem-proving, language-modeling
全部来源与工件
- LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- LeanDojo repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-10
验证历史
- 2023-06-27 · 论文已发布 · E2 · 研究记录
论文公开说明了 LeanDojo、ReProver 与基准方法。
- 2023-06-27 · 论文已发布 · E3 · 可检查工件
开源工具、基准资源与证明器代码被公开，可用于复现与扩展。
更正
当前没有记录的更正。