主要证据
- SorryDB: Can AI Provers Complete Real-World Lean Theorems?S1 · 主要研究来源 · 论文 · 2026-03-03
- SorryDB benchmark, verifier and proving infrastructureS1 · 主要研究来源 · 代码仓库
SorryDB 将真实 Lean 项目的动态证明缺口转化为持续更新的基准
SorryDB 抓取符合条件的公开 Lean 仓库，为尚未完成的 `sorry` 命题记录可复现的仓库与工具链坐标，并要求证明系统在原始项目上下文中填补证明缺口。验证器会重建相应项目并检查候选证明，夜间更新的数据库则持续提供新任务。
发生了什么？
SorryDB 论文发布了一个从 GitHub 上 78 个真实形式化项目提取开放 Lean 任务并动态更新的基准，在 1,000 个任务快照上评测通用模型、专用证明器与 Agent 策略，并公开数据集、验证器和策略基础设施。
为什么重要？
基于真实形式化项目未完成工作的动态基准降低了对已趋饱和竞赛数据集的依赖，暴露合成任务常忽略的依赖关系与环境复杂性，并使证明器进展更直接对应 Lean 贡献者和数学家的实际工作需求。
重要性说明：SorryDB 将形式定理证明评测从以静态整理题集为主的模式，推进到从活跃公开 Lean 项目持续提取、可复现的真实证明任务，直接衡量 AI Agent 能否为实际形式化代码库做出贡献。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化
- AI 贡献
- AI 系统作为候选证明生成器接受评测；它们生成 tactic 或证明，而基准基础设施恢复原始项目上下文，并由 Lean 检查候选替换能否关闭目标证明缺口。
- 人类贡献
- 研究者设计抓取、快照、评测与验证基础设施，定义纳入标准和可复现元数据，实现基线策略并分析基准结果。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- sorrydb, lean
- 机构
- sorrydb
- 数学问题
- real-world-lean-proof-holes, formal-theorem-proving-evaluation
- 方法
- live-benchmarking, repository-crawling, project-context-verification, agentic-proof-search, lean
全部来源与工件
- SorryDB: Can AI Provers Complete Real-World Lean Theorems?S1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- SorryDB benchmark, verifier and proving infrastructureS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2026-03-03 · 论文已发布 · E2 · 研究记录
arXiv 论文发布 SorryDB、其 78 个项目的来源集合、1,000 任务评测快照及不同证明系统的比较结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
SorryDB 公开仓库提供基准快照、夜间数据更新流程、验证器及示例证明策略。E3 表示基准基础设施可直接检查，并不表示所有报告模型分数都获得独立验证。
更正
当前没有记录的更正。