做形式化验证或AI数学推理的团队终于有了应用数学方向的专用基准，比纯代数题更贴近实际工程场景，建议关注其失败模式分析来改进模型。
CAM-Bench是一个新的Lean 4定理证明基准，包含1000个计算与应用数学领域的证明目标，涵盖优化、数值线性代数和数值分析。这些题目改编自教科书习题，依赖局部定义、符号和算法。研究者开发了依赖恢复管道，将每个问题标准化为独立定理并翻译成Lean目标。该基准填补了现有形式化数学基准（如IMO风格问题）的空白，聚焦于应用数学中依赖教科书概念和初等定理的题目。评估显示，现有大模型和形式化代理在跟踪局部假设、应用初等结果、分解证明和长期控制方面存在常见失败模式。
CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
Formal theorem-proving benchmarks enable mechanically verifiable evaluation of mathematical reasoning in large language models. However, existing benchmarks mainly focus on Olympiad-style problems and algebraic domains, leaving computational and applied mathematics underrepresented. We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics, with coverage spanning optimization, numerical linear algebra, and numerical analysis. These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results. To construct CAM-Bench, we develop a dependency-recovery pipeline that reconstructs the local textbook context needed to state each problem faithfully. It then normalizes each problem into a standalone informal theorem and translates it into a Lean target. We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises. For each problem, we release the raw exercise, recovered context, normalized informal theorem, and final Lean target. CAM-Bench complements existing formal mathematics benchmarks by targeting applied mathematics problems that rely on textbook concepts and elementary theorems, many of which are not directly available as standard Mathlib4 lemmas. We evaluate widely used large language models and formalization agents on CAM-Bench, and analyze common failure modes in tracking local assumptions, applying elementary results, decomposing proofs, and maintaining long-horizon control in Lean.