INEQAGENT: Agentic Inequality Proving in Lean with Symbolic Computation

Summary (Overview)

• IneqAgent is an agentic framework that combines LLM reasoning with symbolic computation for formal inequality proving in Lean 4, using lemma-level Monte Carlo Tree Search (MCTS) to coordinate proof search.
• The framework integrates three complementary symbolic backends—sum-of-squares (SOS), Bernstein, and successive difference substitution—that produce exact certificates translated into local Lean proofs.
• On four benchmarks totaling 186 problems, IneqAgent with DeepSeek-V4-Flash solves 175 problems (94.09%), achieving the highest overall success rate among evaluated methods, an improvement of 18.28 percentage points over the strongest baseline (Hilbert at 75.81%).
• IneqAgent achieves higher success rates at low LLM inference cost thresholds (5 and 10 cents) across all four evaluated backbones, with lower mean inference costs over successful runs.
• The framework produces Lean-verified proofs of strengthened Dittert's conjecture in dimensions four and five, and certifies the Holens–Djokovic (4,4) inequality, implying Merris's conjecture in dimension four.

Introduction and Theoretical Foundation

Formal inequality proving requires both mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. Even concise inequalities require carefully chosen substitutions, auxiliary bounds, and substantial algebraic computation. Proving them in Lean requires suitable mathematical strategies and explicit justification of each step, including sign and domain conditions.

Key challenges addressed by the paper:

1. Backend dependency on goal structure: Symbolic backends depend on the goal's algebraic form and assumptions—a rational inequality may require denominator positivity before polynomial reformulation.
2. Computational demands of exact certification: Floating-point candidates from numerical solvers typically satisfy certificate identities only approximately and require exact recovery and verification.

Theoretical foundations include:

• Putinar's Positivstellensatz (1993) for SOS certificates under polynomial constraints
• Kaltofen et al.'s (2012) numerical–symbolic recovery procedure for exact certificates
• Bernstein representations with subdivision (Ray & Nataraj, 2009) for box-constrained problems
• Successive difference substitution (Xia & Yang, 2016) for nonnegative variables

The problem is formalized as establishing:

$$f(\mathbf{x}) \geq 0, \quad \forall \mathbf{x} \in D,\tag{1}$$

where the domain $D$ is specified by constraints:

$$D := \{\mathbf{x} \in \mathbb{R}^n \mid \phi_i(\mathbf{x}) \geq 0, i = 1, \dots, m; \psi_j(\mathbf{x}) = 0, j = 1, \dots, \ell\}.$$

Methodology

Agentic Framework with Lemma-Level MCTS

IneqAgent normalizes the formal statement into standard form and uses a symbol-aware LLM prover based on lemma-level MCTS with the following components:

• Selection (Root-Priority Rule): The root node is expanded until it has $k := B(v)$ child nodes; subsequent exploration selects the highest-scoring child at each level.
• Action (Symbol-Aware Actions): When a node is selected, the agent checks whether the current goal has an algebraic form supported by the symbolic module. If supported, it invokes the symbolic backend; otherwise, it invokes the LLM to generate lemmas and verifies them in Lean.
• Evaluation (Lean Feedback and Proof-Evolution Scoring): The reward function is:

$$r(u) = \left\{ \begin{array}{ll} 1, & \text{if } u \text{ is solved}, \\ 0, & \text{if } u \text{ fails}, \\ \lambda r_u^{\text{Lean}} + (1-\lambda) r_u^{\text{LLM}}, & \text{if } u \text{ is open}. \end{array} \right.$$

where $r_u^{\text{Lean}} \in [0,1]$ is a heuristic progress score based on Lean checking results, and $r_u^{\text{LLM}} \in [0,1]$ assesses progress toward completing the original theorem.

Symbolic Proving Module

The module seeks to establish $p(\mathbf{x}) \geq 0$ for all $\mathbf{x} \in K$ where $K$ is defined by polynomial constraints. Three complementary backends are provided:

1. SOS-based proving searches for a Putinar-type certificate:

$$p = \sigma_0 + \sum_{i=1}^{m} g_i \sigma_i + \sum_{j=1}^{\ell} h_j q_j,\tag{3}$$

where $\sigma_i$ are sums of squares and $q_j$ are unrestricted polynomial multipliers. The approach extends Kaltofen et al.'s recovery procedure to constrained problems through sequential recovery: first recovering rational PSD Gram matrices for inequality multipliers, then recovering $\sigma_0$ and equality multipliers via Gauss–Newton iterations and exact rational recovery.

2. Bernstein-based proving for box-constrained goals uses Bernstein basis polynomials:

$$B_{\mathbf{d},\alpha}(\mathbf{y}) = \prod_{i=1}^{n} \binom{d_i}{\alpha_i} y_i^{\alpha_i}(1-y_i)^{d_i-\alpha_i}, \qquad 0 \leq \alpha_i \leq d_i.\tag{4}$$

The method solves an LP feasibility problem:

$$\text{find } \mathbf{c} \quad \text{subject to } \quad A\mathbf{c} = \mathbf{v}, \quad \mathbf{c} \geq 0.\tag{5}$$

with recursive subdivision when numerical solving fails.

3. Successive difference substitution applies the method of Xia & Yang (2016) for the nonnegative orthant, introducing difference variables:

$$x_{\pi(i)} = \sum_{j=i}^{n} t_j, \quad i = 1, \dots, n, \quad t_j \geq 0.\tag{6}$$

All substitutions and coefficient checks use exact arithmetic, requiring no numerical recovery.

Empirical Validation / Results

Main Benchmark Results

Table 1: Success rate (SR, %) and mean solving time (seconds) across benchmarks

Key results:

• IneqAgent solves 19/20 in MO-INT-20, 46/50 in Ineq-Real, 42/42 in Evan Chen, and 68/74 in LitIneq
• On LitIneq, IneqAgent improves over AxProverBase (strongest baseline there) by 17.57 percentage points
• Mean solving time is substantially lower than LLM-based provers (156.76s vs. 852-1694s for baselines)

Cost Threshold Analysis

Table 2 highlights at 5-cent threshold (SR %):

IneqAgent achieves higher success rates at 5- and 10-cent thresholds across all four backbones, with improvements ranging from 15.59 to 48.92 percentage points at the 5-cent threshold.

Ablation Study

Table 3: Ablation results with DeepSeek-V4-Flash

Both components individually improve performance (168→170 solved problems), and combining them solves 175 problems—five more than either component alone. The full configuration reduces mean LLM inference cost by 70.84% and mean wall-clock time by 52.48% relative to the base agent.

Conjecture Applications

Dittert's conjecture: IneqAgent produces Lean-verified proofs of strengthened inequalities:

$$p_n(A) := 2 - \frac{n!}{n^n} - \Phi_n(A) - \kappa_n \|A - J_n\|_F^2 \geq 0,\tag{7}$$

with $\kappa_4 = 1/52$, $\kappa_5 = 1/2500$, establishing quantitative stability and the unique maximizer $J_n$ in dimensions four and five.

Holens–Djokovic (4,4) inequality:

$$Q_4(A) := 24\operatorname{per}(A) - 2 - \sum_{i,j=1}^{4} a_{ij}^3 \geq 0, \quad A \in \Omega_4.\tag{8}$$

IneqAgent constructs an exact rational SOS certificate for the reduced nine-variable problem, which implies Merris's conjecture in dimension four via:

$$\min_{1 \leq j \leq 4} S_j \leq \frac{1}{4}\sum_{j=1}^{4} S_j = 4\operatorname{per}(A) - \frac{1}{6}Q_4(A) \leq 4\operatorname{per}(A).$$

Theoretical and Practical Implications

• Integration of reasoning paradigms: IneqAgent demonstrates that LLM reasoning and symbolic computation are complementary rather than competing approaches. The lemma-level MCTS provides a principled framework for deciding when to invoke symbolic backends versus LLM-generated steps.

• Extending SOS certification: The sequential recovery procedure extends Kaltofen et al.'s (2012) numerical–symbolic recovery from unconstrained to constrained problems, enabling exact certification of Putinar-type certificates with equality and inequality constraints.

• Cost efficiency: The framework achieves higher success rates at dramatically lower LLM inference costs (e.g., 1.36 cents average vs. 4.67 cents for Direct Agent with DeepSeek-V4-Flash), suggesting that symbolic computation can substitute for expensive LLM reasoning steps.

• Research-level mathematical capability: Producing Lean-verified proofs of strengthened Dittert's conjecture and the Holens–Djokovic inequality demonstrates capability beyond competition problems, extending to open research questions in matrix theory.

• New benchmark: The introduction of LitIneq (74 problems from research papers, polynomial optimization, and Flyspeck) provides a resource for future evaluation of inequality proving systems beyond competition-style problems.

Conclusion

IneqAgent successfully combines lemma-level MCTS with symbolic computation to achieve state-of-the-art results in formal inequality proving in Lean 4. The framework coordinates LLM reasoning, goal reformulation, and symbolic backend selection, integrating certificate-derived local proofs into complete proofs verified against original theorem statements.

Key achievements:

• 94.09% success rate on 186 benchmark problems, surpassing all evaluated baselines
• Lower LLM inference costs across four different backbones
• Lean-verified proofs of strengthened Dittert's conjecture (dimensions 4 and 5) and the Holens–Djokovic (4,4) inequality

The ablation study confirms that both MCTS and symbolic computation contribute meaningfully to performance, with the full system achieving the best results. Future directions may include extending the framework to broader classes of mathematical statements, improving the symbolic backends' coverage of non-polynomial goals, and scaling to larger problem instances.