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

May 14, 2026

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

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.

Ruobing Zuo, Hanrui Zhao, Gaolei He +2

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

Ask PDF

Sep 16, 2025

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

Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called Conjecturing-Proving Loop (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4. A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning. We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously. Moreover, our experiments show that reusing the LLM's own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.

Kazumi Kasaura, Naoto Onda, Yuta Oriike +3

OMRON SINIC X Corporation · RIKEN AIP · AutoRes +7

Automated Theorem Proving In-Context Learning Lean Theorem Proving Language Model Self-Improvement Large Language Model-Guided Theorem Proving

Ask PDF

May 17, 2026

OProver: A Unified Framework for Agentic Formal Theorem Proving

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.

David Ma, Kaijing Ma, Shawn Guo +7

M-A-P

Automated Theorem Proving Lean Theorem Proving LLM Agent Training

Ask PDF

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