AI4Math ChronicleAI4Math 大事记

LeanAgent 将终身学习引入持续演化 Lean 仓库的定理证明

LeanAgent 持续接收新的 Lean 仓库，通过 LeanDojo 抽取定理与前提数据，更新动态数据库，渐进训练前提检索器，并搜索带有 `sorry` 的定理证明；成功证明还可回流知识库供后续学习。

发生了什么？

LeanAgent 论文报告在 23 个 Lean 仓库中为 155 个此前缺少形式证明的定理生成了形式证明，并相较静态定理证明基线改善终身学习中的稳定性与向后迁移表现。

为什么重要？

该工作为 AI 定理证明引入一种持续性的系统视角：数学知识、代码仓库与模型能力共同演化，从而回应“一次训练于静态快照”的证明器难以适应持续增长数学库的问题。

重要性说明：LeanAgent 将神经定理证明重新表述为面向持续演化数学仓库的终身学习问题，而非固定基准任务；它结合动态知识数据库、课程排序和渐进式检索器训练，使证明能力能够跨领域持续保留与扩展。

历史脉络

更早进展
后续进展

—

相关里程碑

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
论文已发布
证据等级
E3 · 可检查工件
AI 角色
AI 主导、人类核验
形式保障
机器检查

如何理解这些标签？ →

贡献与验证

数学新颖性
工具性进展
接口
形式化, 符号
AI 贡献
学习式前提检索与 tactic 生成驱动跨 Lean 仓库的自动证明搜索，Lean 则机械检查候选 tactic 序列并接受成功的形式证明。
人类贡献
研究者设计终身学习架构、仓库课程、动态数据库与渐进训练流程，选择评测仓库，并分析稳定性与迁移表现。
验证状态
论文已发布 · E3 · 可检查工件 · 机器检查
最后审阅
2026-09-11

技术细节

系统
leanagent, lean, leandojo
机构
caltech
数学问题
lean-theorem-proving
方法
lifelong-learning, continual-learning, premise-selection, curriculum-learning, proof-search

全部来源与工件

验证历史

  • 2024-10-08 · 论文已发布 · E2 · 研究记录

    arXiv 研究记录发布 LeanAgent，并报告其跨多个 Lean 仓库的持续学习与形式证明结果。

  • 2026-09-11 · 论文已发布 · E3 · 可检查工件

    公开的 LeanAgent 仓库提供实现、测试与复现实验配置，该工作后来发表于 ICLR 2025。machine-checked 表示生成的形式证明由 Lean 接受，并不表示完整实验已获独立重放，也不表示产生了新的非形式数学结果。

更正

当前没有记录的更正。