CAM-Bench：Lean中的计算与应用数学基准

形式化定理证明基准可以对大语言模型的数学推理进行机器可验证的评估。然而，现有基准主要聚焦奥赛风格问题和代数领域，计算与应用数学的覆盖不足。我们提出CAM-Bench，一个包含1000个计算与应用数学Lean证明目标的Lean 4定理证明基准，覆盖范围横跨优化、数值线性代数和数值分析。这些问题改编自教科书习题，往往依赖局部引入的定义、记号、算法和初等结果。为构建CAM-Bench，我们开发了依赖恢复流水线，重建忠实陈述每个问题所需的局部教科书上下文。随后将每个问题规范化为独立的非形式化定理，并翻译为Lean证明目标。我们通过Lean编译和语义审查验证所得形式化问题，同时检查形式正确性和与原始习题的语义一致性。对每个问题，我们发布原始习题、恢复的上下文、规范化的非形式化定理和最终的Lean证明目标。CAM-Bench聚焦依赖教科书概念和初等定理的应用数学问题——其中许多无法直接以标准Mathlib4引理获得——从而补充了现有形式化数学基准。我们在CAM-Bench上评估了广泛使用的大语言模型和形式化智能体，并分析了在追踪局部假设、应用初等结果、分解证明以及在Lean中保持长程控制方面的常见失败模式。