Papers With

← All papers
First page of IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang

cs.AI Oct 14, 2026 · v1
ai-agents theorem-proving-ml benchmark analysis
Read PDF arXiv abstract Code
TL;DR
Builds an LLM agent that generates Lean 4 inequality proofs from symbolic certificates, with every proof checked by the Lean kernel against the original theorem statements.
Abstract
Formal inequality proving requires mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. We introduce IneqAgent, an agentic framework combining LLM reasoning with symbolic computation for inequality proving in Lean4. Lemma-level Monte Carlo Tree Search coordinates lemma construction, goal reformulation, and symbolic backend selection. Complementary sum-of-squares, Bernstein, and successive difference-substitution backends produce exact certificates for local Lean proof generation. The agent integrates these proofs with LLM-generated steps and uses Lean feedback to construct complete proofs checked against the original theorem statements. On four benchmarks, IneqAgent with DeepSeek-V4-Flash solves 175 of 186 problems (94.09%), achieving the highest overall success rate among the evaluated methods. Across four backbones, it achieves higher success rates at low LLM inference cost thresholds than Direct Agent using the same backbone, with lower mean inference costs over each method's successful runs. We also obtain Lean-verified strengthenings of Dittert's conjecture in dimensions four and five, and certify the Holens–Djokovic $(4,4)$ inequality, implying Merris's conjecture in dimension four.
Problem

Formal inequality proving in Lean needs both mathematical strategy and exact algebraic computation, including side conditions such as signs and domains. LLMs and symbolic certificate methods each cover part of this, but combining them is hard. Symbolic backends depend on the goal's algebraic form, and numerical certificates must be recovered exactly.

Approach

IneqAgent uses lemma-level Monte Carlo Tree Search to coordinate lemma construction, goal reformulation and symbolic backend selection. It has three backends that produce exact certificates turned into local Lean proofs. These are sum-of-squares with Putinar-type certificates and sequential recovery under constraints, Bernstein polynomials with linear programming and subdivision for box constraints, and successive difference substitution for nonnegative variables. The agent merges these local proofs with LLM-generated steps and uses Lean diagnostics to guide further attempts. The authors also build LitIneq, a benchmark of 74 Lean 4 tasks drawn from research papers and from Flyspeck proof obligations.

Results

Using DeepSeek-V4-Flash, IneqAgent solves 175 of 186 problems (94.09%) across MO-INT-20, Ineq-Real, Evan Chen and LitIneq, the highest overall rate among evaluated methods. With each of four backbones, it beats a Direct Agent on success rate at low inference-cost thresholds. It also gives Lean-verified strengthenings of Dittert's conjecture in dimensions 4 and 5, and certifies the Holens–Djokovic (4,4) inequality, which implies Merris's conjecture in dimension 4.

BackboneMethodSR @5¢SR @10¢SR no capCost no cap
DeepSeek-V4-FlashDirect Agent66.6779.0390.324.6700
DeepSeek-V4-FlashIneqAgent88.1792.4794.091.3619
Qwen3.8-FlashDirect Agent68.2884.4193.554.7061
Qwen3.8-FlashIneqAgent83.8789.2592.471.5543
Success rate (%) and mean cost (US cents) at selected LLM inference cost thresholds (excerpt; 186 problems)