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

• URL: http://arxiv.org/abs/2605.17255v1
• Date: Sun, 17 May 2026 04:53:47 GMT
• Title: CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
• Abstract summary: We introduce CAM-Bench, a Lean 4 theorem-proving benchmark of 1,000 Lean proof targets in computational and applied mathematics.<n>These problems are adapted from textbook exercises and often depend on locally introduced definitions, notation, algorithms, and elementary results.<n>We validate the resulting formal problems through Lean compilation and semantic review, checking both formal correctness and semantic alignment with the original exercises.
• Score: 10.684401671916158
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
  MathAdv is a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics.<n>We show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures.
  arXiv  Detail & Related papers  (2026-08-26T07:12:54Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis [28.906916840252077]
  MA-ProofBench is the first formal theorem-proving benchmark dedicated to Mathematical Analysis.<n>The benchmark contains 200 formalized theorems covering 6 core topics and 27 subcategories, including measure and integration theory, complex analysis, and functional analysis.<n>We evaluate a range of recent general-purpose reasoning models and formal theorem provers on MA-ProofBench.
  arXiv  Detail & Related papers  (2026-06-11T18:00:04Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  We evaluate the robustness of current ATP systems when applied to a novel definitional framework.<n>We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I.<n>For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem.
  arXiv  Detail & Related papers  (2026-03-13T07:39:47Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch [8.80477323574638]
  We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving.<n>IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads.
  arXiv  Detail & Related papers  (2025-11-30T17:40:13Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  We present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems.<n>We introduce a novel human-in-the-loop autoformalization pipeline that integrates statement autoformalization, semantic verification, and negation-based disproof filtering strategies.<n>Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations.
  arXiv  Detail & Related papers  (2025-05-05T15:37:00Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATH is a novel Olympiad-level mathematical benchmark designed to rigorously test the complex reasoning capabilities of LLMs.<n>OlymMATH features 200 meticulously curated problems, each manually verified and available in parallel English and Chinese versions.
  arXiv  Detail & Related papers  (2025-03-27T11:20:17Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  We present LeanAgent, a novel lifelong learning framework for formal theorem proving.<n>LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge.<n>It generates formal proofs for 155 theorems across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  This paper explores the use of Large Language Models (LLMs) to generate formal proof steps and complete formalized proofs. The goal is to determine how AI can be leveraged to assist the mathematical formalization process and improve its performance.
  arXiv  Detail & Related papers  (2024-09-09T18:21:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.