Technical Summary: Construction–Verification: A Benchmark for Formalizing Applied Mathematics in Lean 4

1. Problem Statement

Current benchmarks for automated theorem proving, such as MiniF2F and ProofNet, predominantly focus on the logical verification of declarative propositions (i.e., proving the existence of a solution). This paradigm is insufficient for applied mathematics, where the primary objective is often the derivation of concrete values, executable algorithms, or structural transformations rather than mere existence proofs.

Existing datasets suffer from two critical limitations in this domain:

1. Scope Gap: They lack coverage of undergraduate-level and higher applied mathematics, including convex analysis, optimization, numerical algebra, and high-dimensional probability.
2. Constructive Deficit: They fail to enforce a "construction-verification" workflow. In applied mathematics, a model must explicitly synthesize a solution (e.g., an algorithm or a specific value) before proving its correctness. Current benchmarks allow models to bypass this by using non-constructive tactics (e.g., proving existence via the extreme value theorem without calculating the specific optimum), thereby misrepresenting the model's ability to perform computational reasoning.

2. Methodology

The Construction–Verification Framework

The authors propose a formalization paradigm in Lean 4 that structurally enforces a two-stage workflow: Construction followed by Verification. This framework prevents agents from exploiting non-constructive shortcuts by requiring explicit definitions before proofs. The framework addresses three specific categories of applied mathematical tasks:

• Evaluation Problems: Instead of proving $\exists x, Q(x)$, the agent must define a function def x (V) := ... that computes the solution $x(V)$ based on parameters $V$, followed by a theorem proving $Q(x(V), V)$. The function signature strictly restricts inputs to raw parameters, preventing the model from using the target property to "cheat" the construction.
• Algorithm Design Problems: The agent must define a recursive function representing an iterative process (e.g., Gradient Descent). The task requires filling in the transition rule (the loop body) for the $(n+1)$-th step, followed by a proof of properties like convergence or monotonicity.
• Representation Transformation: The agent must model a raw problem instance as a target canonical form (e.g., transforming a graph cut problem into a spectral clustering formulation). This involves defining the new domain, constraints, and objective function, and proving a relaxation or equivalence relation between the source and target problems.
• Theorem Proving: A baseline subset of traditional deductive tasks is included to measure pure logical reasoning capabilities distinct from constructive synthesis.

Benchmark Curation (AMBER)

The authors introduce AMBER (Applied Mathematics BEnchmark for Reasoning), a dataset spanning four core domains:

1. Convex Analysis
2. Optimization
3. Numerical Algebra
4. High-Dimensional Probability

Data Sources & Difficulty: Problems are sourced from classical textbooks (e.g., Boyd & Vandenberghe, Vershynin) and categorized by difficulty (Easy: standard exercises; Hard: PhD qualifying exam level).
Formalization & Validation: 50 problems per subfield were formalized by experienced Lean users. Validation involved a two-stage process: an LLM-based semantic check followed by rigorous manual cross-validation by Mathlib contributors to ensure strict alignment with original mathematical statements.
Complexity Metrics: The benchmark is characterized by high semantic dependency density. Using a dependency graph analysis ($k=3$), AMBER exhibits an average dependency density of 164.21, significantly higher than MiniF2F (29.72), ProofNet (33.95), and FATE (53.14), indicating a deeper requirement for retrieving and reasoning over complex mathematical concepts.

3. Key Contributions

1. Paradigm Shift: The paper proposes a shift from verifying existential propositions to synthesizing constructive solutions, aligning formal tasks with the computational intuition of applied mathematics.
2. AMBER Benchmark: A comprehensive dataset covering core applied domains with varying difficulty levels, featuring complex tasks like algorithm design and representation transformation, not just theorem proving.
3. Formalization Patterns: Specialized Lean 4 templates for evaluation, algorithm design, and representation transformation that enforce strict syntactic barriers against non-constructive reasoning.
4. Empirical Analysis: A systematic evaluation revealing a fundamental trade-off in current neuro-symbolic systems: the tension between local tactical proficiency (specialized provers) and high-level algorithmic synthesis (general models).

4. Experimental Results

Model Performance

The authors evaluated a diverse set of models, including general-purpose reasoning agents (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) and specialized theorem provers (Goedel Prover-32B, Kimina Prover-72B).

• Overall Difficulty: Performance across all models is remarkably low. On the "Hard" subset, success rates are near zero for almost all models.
• General vs. Specialized: Contrary to the trend in pure mathematics benchmarks, general-purpose reasoning models consistently outperform specialized theorem provers.
  • Pass@16 (Full AMBER): General models achieved 4.50%–6.00%, while specialized provers achieved 4.00%.
  • Pass@16 (Hard Subset): General models achieved 0%–0% (with some variation in Easy subsets), while specialized provers also struggled significantly.
• Ablation Study: The construction-verification prompt strategy yielded an 8% success rate on a 100-problem subset, outperforming standard code completion (6%) and traditional proof-only prompts (5%). Proof-only prompts frequently led models to use non-constructive shortcuts (e.g., Classical.choice).

Error Analysis

An analysis of 3,189 error messages from the DeepSeek-R1 model revealed:

1. Hallucination (47.3%): The most common failure mode, where models invoke non-existent theorems or definitions (e.g., convexHull eq sInter).
2. Formalization Competence (32.7%): Misapplication of valid tactics or failure to discharge side-conditions.
3. Incomplete Outputs (15.2%): Failure to provide fully executable code, often leaving sorry placeholders in complex inductive steps.
4. Formatting/Syntax (4.8%): Basic markdown or syntax errors.

5. Significance and Claims

The paper claims that the current landscape of automated formalization faces a "tactical overfitting" phenomenon. Specialized models, fine-tuned extensively on proof corpora, appear to degrade their general instruction-following capabilities. They treat every structural challenge as a pure theorem-proving task, often ignoring the multi-stage requirements of applied mathematics (e.g., defining a function before proving it).

In contrast, general-purpose models retain the versatility required to bridge informal intent and formal syntax, successfully synthesizing mathematical objects before entering the verification stage. The authors conclude that advancing formalized applied mathematics requires moving beyond pure proof search toward neuro-symbolic systems that integrate high-level algorithmic reasoning with rigorous formal verification. The AMBER benchmark serves as a foundation for future research in expanding the frontiers of formalized applied mathematics by providing a standard that demands constructive synthesis rather than mere logical validity.