arXiv cs.AI@Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen精选58CAM-Bench是一个新的Lean 4定理证明基准，包含1000个计算与应用数学领域的证明目标，涵盖优化、数值线性代数和数值分析。这些题目改编自教科书习题，依赖局部定义、符号和算法。研究者开发了依赖恢复管道，将每个问题标准化为独立定理并翻译成Lean目标。该基准填补了现有形式化数学基准（如IMO风格问题）的空白，聚焦于应用数学中依赖教科书概念和初等定理的题目。评估显示，现有大模型和形式化代理在跟踪局部假设、应用初等结果、分解证明和长期控制方面存在常见失败模式。论文定理证明Lean 4基准测试应用数学形式化验证推荐理由：做形式化验证或AI数学推理的团队终于有了应用数学方向的专用基准，比纯代数题更贴近实际工程场景，建议关注其失败模式分析来改进模型。