CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen
Abstract
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.
AI Impact Assessments
(1 model)Scientific Impact Assessment: CAM-Bench
1. Core Contribution
CAM-Bench addresses a genuine gap in formal mathematics benchmarking: the underrepresentation of computational and applied mathematics. While existing benchmarks (MiniF2F, PutnamBench, ProofNet, FormalMATH) focus primarily on Olympiad-style problems or algebraic domains, CAM-Bench targets textbook exercises in optimization, numerical linear algebra, and numerical analysis. The key novelty is twofold: (a) the benchmark itself—1,000 Lean 4 proof targets derived from 778 textbook exercises with full provenance chains, and (b) a dependency-recovery pipeline that reconstructs the local textbook context (definitions, notation, algorithms, assumptions) needed to faithfully state each problem as a self-contained Lean target.
The dependency-recovery pipeline is the more technically interesting contribution. Textbook exercises in applied mathematics are rarely self-contained—they reference earlier definitions, algorithms, and conventions. The recursive dependency expansion (Algorithm 1) with source-grounded enrichment, followed by modularization into semantic blocks and frozen-context incremental formalization, represents a systematic approach to a genuinely difficult problem in benchmark construction.
2. Methodological Rigor
The construction pipeline is carefully designed with multiple validation layers: source-level semantic review (accept/revise/hold classification), Lean compilation checking, and Lean-level semantic validation. The conservative funnel approach—only 54.3% of candidates survive source-level review, and 92.5% of Lean declarations pass semantic validation—suggests quality control was taken seriously.
However, several concerns arise. The semantic review relies heavily on "LLM-as-a-judge," which introduces potential systematic biases that are difficult to characterize. While the authors acknowledge this as a "diagnostic signal" rather than a "sole correctness criterion," the pipeline's integrity still depends substantially on LLM judgment at multiple stages. The paper does not report any human expert validation of a random sample of final Lean targets, which would significantly strengthen confidence in benchmark quality.
The experimental evaluation is reasonable but not exhaustive. The pass@32 protocol for non-agentic baselines and the 8-hour budget for agentic systems provide meaningful comparisons. The external agent evaluation (M2F and Aristotle) on 200 sampled instances is a useful addition, though the sample size limits statistical power for fine-grained analysis.
3. Potential Impact
Benchmark impact: CAM-Bench fills a real niche. Applied mathematics formalization is fundamentally different from competition mathematics—it requires tracking inherited assumptions, working with domain-specific infrastructure (matrices, spectra, convexity, convergence), and managing longer proof chains with more auxiliary definitions. The benchmark should motivate development of better Mathlib infrastructure for applied mathematics and better handling of context-dependent formalization.
Pipeline contribution: The dependency-recovery pipeline could be adapted beyond this specific benchmark to other textbook-to-formal translation tasks. The semantic block decomposition and frozen-context construction approach are general techniques.
Diagnostic value: The error analysis identifying three failure categories (Library/API grounding, formal representation/type discipline, proof decomposition/long-horizon control) provides actionable insights. The finding that 68-69% of agentic system failures involve proof decomposition and long-horizon control is particularly informative.
Limitations on impact: The benchmark is heavily optimization-centric despite claiming to cover "computational and applied mathematics" broadly. PDEs, control theory, scientific computing, and other major applied mathematics areas are absent. The practical barrier to adoption may be high since many problems require infrastructure not yet in Mathlib4.
4. Timeliness & Relevance
The paper is well-timed. Formal theorem proving with LLMs is advancing rapidly (DeepSeek-Prover, SEED-Prover, various agentic systems), and there is increasing recognition that Olympiad-focused benchmarks do not capture the full spectrum of mathematical reasoning capabilities. The informal-formal gap documented here (70-84% informal accuracy vs. 2-20% verified Lean accuracy for non-agentic baselines) powerfully demonstrates that current models can reason about applied mathematics but cannot ground those arguments in formal infrastructure—a critical finding for the field.
The evaluation includes very recent models (GPT-5.4, Claude-sonnet-4.6, Deepseek-v4-pro, Gemini-3.1-pro-preview, Kimi-k2.6) and state-of-the-art agentic systems (M2F, Aristotle), making the results immediately relevant.
5. Strengths & Limitations
Strengths:
Limitations:
Additional Observations
The dataset release with full intermediate artifacts (raw exercise, recovered context, normalized theorem, final Lean target) is commendable and enables community auditing. The strict validation protocol for agentic systems (checking for sorry, admit, axiom, etc.) is well-designed. The observation that agentic repair increases GPT-5.4 from 11.7% to 44.0% at ~3x token cost provides useful efficiency analysis.
Generated May 19, 2026
Comparison History (23)
Paper 1 likely has higher scientific impact due to its durable, broadly reusable infrastructure contribution: a 1,000-problem Lean 4 benchmark filling a clear gap (computational/applied math) and enabling mechanically verifiable evaluation of LLM mathematical reasoning. Its dependency-recovery pipeline and artifact release (exercise→context→informal theorem→Lean target) support reproducibility and future research across formal methods, AI evaluation, and mathematical libraries. Paper 2 is timely and application-relevant, but dataset/task + prompting framework for ToM persuasion is more domain-specific, potentially more sensitive to annotation subjectivity, and may age faster with model advances.
Paper 1 introduces a novel benchmark for formal theorem proving in Lean 4, addressing a critical bottleneck in AI reasoning by expanding beyond pure mathematics into applied domains. High-quality formal benchmarks are highly foundational, widely adopted by the AI community to evaluate reasoning limits, and typically garner broad scientific impact. Paper 2 offers valuable contributions to Theory of Mind and conversational agents, but targets a narrower subfield of persuasive dialogue compared to the broad utility of evaluating and advancing general logical reasoning.
Paper 1 proposes a fundamental paradigm shift in the architecture of AI agents, moving from LLM-centric loops to event-sourced reactive graphs. This addresses critical challenges in agent observability, determinism, and state management, offering broad applicability across AI safety, self-improving systems, and enterprise software. While Paper 2 provides a valuable formal mathematics benchmark, it represents an incremental contribution to a specific sub-field. Paper 1's architectural innovation has a much higher ceiling for widespread adoption and transformative impact across the broader AI and software engineering communities.
CAM-Bench addresses a clear gap in formal theorem-proving benchmarks by targeting computational and applied mathematics, an underrepresented domain. It provides a rigorous, large-scale benchmark (1,000 problems) with a validated pipeline, enabling reproducible evaluation of LLMs on applied math reasoning. This fills a concrete need in the AI-for-mathematics community and will likely drive research progress. Paper 2 describes an architectural proposal (ActiveGraph) for agent systems with interesting properties (replay, forking, lineage), but it is more of a position/design paper without demonstrated empirical results, limiting its immediate scientific impact.
Paper 2 addresses a highly timely and rapidly expanding field: evaluating Large Language Models' mathematical reasoning using formal verification (Lean 4). By providing a novel benchmark for computational and applied mathematics, it serves a critical need in AI development and is likely to be widely adopted and cited. Paper 1, while methodologically sound, operates in a much narrower and established subfield of information fusion and belief functions, limiting its broader scientific impact compared to the AI/LLM benchmark.
Paper 2 likely has higher scientific impact: it contributes a large, reusable Lean 4 benchmark (1,000 targets) addressing a clear gap (computational/applied math) with rigorous validation (compilation + semantic review) and rich artifact release, enabling standardized, reproducible evaluation across many future models and agents. Its breadth spans formal methods, ML, and applied mathematics, and it is timely given rapid growth in LLM theorem proving. Paper 1 is innovative but more system-integration/proof-of-concept and depends on specific tools/models, which may limit reproducibility and long-term generality.
CAM-Bench likely has higher scientific impact because it provides a broadly reusable community resource (1,000 Lean 4 targets) that enables standardized, mechanically verifiable evaluation of LLM mathematical reasoning in undercovered applied/computational domains. Its dependency-recovery/normalization pipeline and released artifacts can catalyze follow-on work in formalization, benchmarking, curriculum learning, and tool development across ML, PL, and mathematics. SAPO is a solid methodological improvement for RL credit assignment in generative recommendation, with clear practical value, but its impact is narrower to a specific task/setup and may be more incremental.
DARE-EEG addresses a critical challenge in Brain-Computer Interfaces by developing a highly transferable foundation model for EEG data. Its potential real-world applications in healthcare, neurology, and cognitive science offer broader scientific impact than CAM-Bench, which, while valuable for AI-driven formal theorem proving, serves a more niche community. Foundation models for physiological signals represent a highly impactful and rapidly growing cross-disciplinary field.
CAM-Bench addresses a significant gap in formal theorem-proving benchmarks by targeting computational and applied mathematics, an underrepresented area. It provides a reusable community resource (1,000 Lean proof targets) that can drive progress in AI mathematical reasoning, a rapidly growing field. Its breadth of impact spans formal verification, AI/LLM evaluation, and applied mathematics. Paper 1, while solid, addresses a more niche problem (sleep stage classification) with incremental methodological contributions. CAM-Bench's timeliness—given the surge in LLM reasoning research—and its potential to become a widely-used benchmark give it higher impact potential.
Paper 1 introduces a mechanically verifiable benchmark for LLMs in an underrepresented domain (applied and computational mathematics) using Lean 4. Its reliance on formal theorem proving provides a rigorous, hallucination-free evaluation metric, which is critical for the reliable advancement of AI in mathematics. While Paper 2 offers a useful methodology for improving logicality in physics QA, Paper 1's contribution to formal verification addresses a more fundamental bottleneck in AI scientific reasoning, likely yielding broader, longer-lasting impact across AI and applied mathematics.