arxiv-2605-17255 SRC-0358 · paper

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

Created: 2026-05-17 · Ingested: 2026-09-19

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 definition

In brief

Frontier models can state applied-math arguments informally far better than they can verify them in Lean, and the gap is large: informal pass@1 of 70.0%-83.8% against verified Lean accuracy below 20% at pass@32.

CAM-Bench is 1,000 Lean 4 proof targets drawn from 778 textbook exercises in optimization, numerical linear algebra, and numerical analysis, built by a dependency-recovery pipeline that reconstructs local definitions, notation, and inherited assumptions before formalization. Success is file-level: every sorry in a file must be filled and the file must compile.

Among non-agentic pass@32 baselines, Deepseek-v4-pro reaches 19.67%, Claude-sonnet-4.6 19.28%, Gemini-3.1-pro-preview 18.38%, GPT-5.4 11.70%, Kimi-k2.6 2.25%. An agentic repair harness takes GPT-5.4 to 44.00%, at about 1.96M tokens per instance versus 0.26-0.70M for the baselines. On 200 sampled instances with an 8-hour budget each, M2F solves 143/200 (71.5%) and Aristotle 125/200 (62.5%).

The agentic comparison holds the instance set, wall-clock budget, and validation script fixed, and rejects sorry, axiom, or statement-altering artifacts. The pass@32 and agentic settings are not matched on token budget, so the 11.70%-to-44.00% jump confounds scaffolding with compute. Failure labels are multi-label and hand-assigned; construction quality rests on LLM-as-a-judge review (92.5% of Lean declarations judged usable).

Use this if you want a formal benchmark where Mathlib coverage, not competition-style cleverness, is the binding constraint.

Written from the abstract by claude-opus-5 on 2026-10-24, with every figure checked against it. Not a substitute for the paper.

Referenced by

Claims in this catalog that draw on this source, and whether as support or counterpoint.

supportsOn 1,000 Lean 4 targets from computational and applied mathematics textbooks (optimization, numerical linear algebra, numerical analysis), whose statements depend on locally introduced definitions, current provers solve about 62-72% of a 200-problem sample, so applied-math formalization is tractable but not saturated and requires recovering textbook context to state problems faithfully.