IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

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

cs.AIOct 14, 2026

IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

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

Organizations: School of Software Engineering, East China Normal University · School of Computer and Information Science, Southwest University

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.

Figures & tables

Figure 1: Overview of IneqAgent. The agent normalizes the formal statement and assesses each goal for symbolic computation. It develops intermediate lemmas when further reasoning is needed, coordinates tool calls, and integrates local proofs into the current proof context. Symbolic feedback and Lean diagnostics guide subsequent attempts until the original theorem is proved.

Symbolic computation
	MO-INT-20		Ineq-Real		Evan Chen		LitIneq		Overall
Method	SR	Time	SR	Time	SR	Time	SR	Time	SR	Time
Z3	25.00	234.20	30.00	20.04	42.86	0.15	55.41	1.80	42.47	19.59
Maple	0.00	–	10.00	1.69	26.19	1.28	41.89	152.60	25.27	101.132
Isabelle sos	0.00	–	4.00	21.69	9.52	21.69	21.62	18.90	11.83	19.66
LLM provers

Table 1: Success rate (SR, %) and mean solving time over problems successfully solved by each method (Time, seconds). Overall aggregates all 186 problems; its mean time is weighted by the number of successful problems in each benchmark. Bold indicates the highest success rate in each benchmark and overall. A dash indicates that no problem was solved.

		LLM inference cost threshold (US cents)
		5		10		50		100		No cap
Backbone	Method	SR	Cost	SR	Cost	SR	Cost	SR	Cost	SR	Cost
DeepSeek-V4-Flash	Direct Agent	66.67	1.9499	79.03	2.7609	90.32	4.6700	90.32	4.6700	90.32	4.6700
	IneqAgent (ours)	88.17	0.6773	92.47	0.9485	94.09	1.3619	94.09	1.3619	94.09	1.3619
Qwen3.8-Flash	Direct Agent	68.28	1.7882	84.41	2.7370	92.47	4.0352	93.55	4.7061	93.55	4.7061
	IneqAgent (ours)	83.87	0.8219	89.25	1.1747	92.47	1.5543	92.47	1.5543	92.47	1.5543

Table 2: Proof success and LLM inference cost on 186 problems. Both methods use the backbone specified in the first column. All thresholds and mean costs are in US cents. SR (%) is the percentage of all 186 problems solved with cumulative LLM inference cost at or below the specified threshold; Cost is the mean cost over those successful runs. Thresholds are applied post hoc. No cap includes all successful runs and the two-hour per-problem limit still applies. Within each backbone and threshold, the highest SR is bold; the lower Cost is bold when both means are defined.

Variant	SR (%) $\uparrow$	Avg. LLM cost (US cents) $\downarrow$	Avg. time (s) $\downarrow$
Base agent	90.32	4.6700	329.88
Base + MCTS	91.40	2.2251	191.64
Base + Symbolic	91.40	2.8514	200.56
IneqAgent (full)	94.09	1.3619	156.76

Table 3: Ablation results with DeepSeek-V4-Flash on all 186 benchmark problems under a two-hour time limit per problem. Mean LLM inference cost and wall-clock time are computed over each variant’s successful problems. Bold indicates the highest success rate or the lowest reported mean.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Parameter	Meaning	Value
$\kappa$	Progressive-widening scale	$1.0$
$\alpha$	Progressive-widening exponent	$0.5$
$c$	Exploration coefficient	$1.414$
$\lambda$	Weight of the Lean-based reward	$0.5$
$\rho$	Stagnation penalty per attempt	$0.06$
$\rho_{\max}$	Maximum stagnation penalty	$0.30$

Appendix

Table 4: Default parameters for lemma-level search.

Condition	Contribution to $h$
Candidate compiles ( $b=1$ )	$+0.35$
Proof text changed ( $e=1$ )	$+0.10$
Proof text unchanged ( $e=0$ )	$-0.12$
Change in unfinished-marker count	$\max\{-0.30,\min\{0.30,0.18\Delta\}\}$
$m_{u^{\prime}}>0$ unfinished markers remain	$-\min\{0.20,0.04m_{u^{\prime}}\}$
$a>0$ new structured steps	$+\min\{0.20,0.05a\}$

Appendix

Table 5: Additive terms in the Lean-based heuristic. Agent execution refers to the proving-agent invocation for the current expansion.

Source group	Count	Instances and source attributions
Bernstein examples	2	Coefficient and subdivision examples
APPIRL benchmark	2	C1–C2: Verschelde (1996), Polynomial homotopy continuation: A portable Ada software package ( Verschelde, 1996 )
APPIRL benchmark	1	C3: Iserles (1995), personal communication at the AMS–SIAM summer seminar ( Iserles, 1995 )
APPIRL benchmark	2	C4, C6: Noonburg (1989), A neural network modeled by an adaptive Lotka–Volterra system ( Noonburg, 1989 )
APPIRL benchmark	1	C5: Verschelde (2001), The PHC Pack, the database of polynomial systems ( Verschelde, 2001 )
APPIRL benchmark	1	C7: Faugère (1999), A new efficient algorithm for computing Gröbner bases (F4) ( Faugère, 1999 )

Appendix

Table 6: Collection sources and source attributions for the 74 LitIneq instances. C1–C10 attributions follow APPIRL.

	Target total degree $d_{p}$
Variables $n$	$0$ – $2$	$3$ – $4$	$5$ – $8$	Total
$1$ – $2$	6	2	2	10
$3$ – $4$	4	9	0	13
$5$ – $6$	7	7	3	17
$7$ – $8$	4	2	2	8
$11$	0	1	0	1

Appendix

Table 7: Distribution of the 49 polynomial instances by the number of variables

n

and target total degree

d_{p}

. Entries are instance counts. We count all quantified real variables, including parameters, without eliminating fixed variables. The degree is computed after expanding auxiliary definitions, simplifying rational constants, and moving the target to one side.

Backbone	Input	Cached input	Output
DeepSeek-V4-Flash	0.2206	0.0074	0.6618
Qwen3.8-Flash	0.1176	0.0147	0.3971
Kimi-K3	2.9412	0.2941	14.7059
GPT-5.5	5.0000	0.5000	30.0000

Appendix

Table 8: LLM inference rates in USD per million tokens. Input denotes uncached input tokens.

Task	Variables	Total degree	Monomials	Time (s)	Cost (US cents)
Dittert, $n=4$	16	4	521	5,292	84.6728
Dittert, $n=5$	25	5	118,755	6,704	100.1654
HD $(4,4)$	9	4	222	42,731	521.9610

Appendix

Table 9: Conjecture task sizes and costs. Dittert sizes refer to

P_{4}

and

\widetilde{F}_{5}

before constraint elimination. For HD

(4,4)

, sizes refer to the reduced Holens–Djokovic polynomial

Q_{4}

, using the upper-left

3\times 3

entries as nine independent variables. Time is wall-clock time and Cost is total LLM inference cost.

Lean Theorem Proving

Lean theorem proving uses the Lean proof assistant to construct machine-checked mathematical proofs, often with automated search and language models.

See all 123 papers

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
May 14, 2026Ruobing Zuo, Hanrui Zhao, Gaolei He +2Mathematical Reasoning Neuro-Symbolic Reasoning
School of Software Engineering, East China Normal University, Shanghai, China · College of Computer Science and Technology, National University of Defense Technology, Changsha, China · School of Computer and Information Engineering, Henan University, Kaifeng, China
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Sep 16, 2025Kazumi Kasaura, Naoto Onda, Yuta Oriike +3Automated Theorem Proving In-Context Learning
OMRON SINIC X Corporation · RIKEN AIP · AutoRes +7
OProver: A Unified Framework for Agentic Formal Theorem Proving
May 17, 2026David Ma, Kaijing Ma, Shawn Guo +7Automated Theorem Proving Lean Theorem Proving
M-A-P

May 14, 2026J/K move · Enter open · S save

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang+1

School of Software Engineering, East China Normal University, Shanghai, China · College of Computer Science and Technology, National University of Defense Technology, Changsha, China · School of Computer and Information Engineering, Henan University, Kaifeng, China

Mathematical Reasoning Neuro-Symbolic Reasoning LLM Mathematical Reasoning

Open paper AskPDF arXiv

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.

Abstract

Lean Theorem Proving

Explore similar work

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

OProver: A Unified Framework for Agentic Formal Theorem Proving