论文
SorryDB：AI 证明器能否完成真实世界的 Lean 定理？
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
摘要
我们提出 SorryDB，一个动态更新的开放 Lean 任务基准，任务取自 GitHub 上 78 个真实形式化项目。与常由竞赛题构成的既有静态基准不同，在 SorryDB 上爬山优化将产出贴近社区需求、对数学家更可用、更善于理解复杂依赖的工具。此外，通过提供持续更新的任务流，SorryDB 缓解测试集污染，并为智能体对新形式化数学项目做出贡献的能力提供稳健指标。我们在 SorryDB 选定的 1000 个任务快照上评估多种方法，包括通用大语言模型、Agentic 方法和专用符号证明器。我们表明当前方法各有互补：尽管基于 Gemini Flash 的 Agentic 方法表现最佳，但它并非严格优于其他现成大语言模型、专用证明器，甚至精选的 Lean 战术列表。
