IneqSearch: Hybrid Reasoning for Olympiad Inequality Proofs
Authors: Zhaoqun Li
Beishui Liao
Qiwei Ye
Venue: NeurIPS 2025 poster ()
Keywords: Olympiad Inequality Proving
Neuro-Symbolic Method
Primary area: other

Abstract: Mathematicians have long employed decomposition techniques to prove inequalities, yet automating this process remains a significant challenge in computational mathematics. We introduce IneqSearch, a hybrid reasoning system that integrates symbolic computation with large language models (LLMs) to address this challenge. IneqSearch reformulates inequality proving as a structured search problem: identifying appropriate combinations of theorems that decompose expressions into non-negative components. The system combines a symbolic solver for deductive reasoning with an LLM-based agent for constructive proof exploration, effectively implementing methodologies observed in formal mathematical practice. A key contribution of IneqSearch is its iterative learning mechanism that systematically incorporates newly proven results into its theorem database, enabling knowledge acquisition during practice that enhances its capabilities without requiring human intervention. In empirical evaluation on 437 Olympiad-level inequalities, IneqSearch successfully proves 342 problems, significantly outperforming existing methods and demonstrating the effectiveness of integrating symbolic and neural approaches for mathematical reasoning.

IneqSearch: Hybrid Reasoning for Olympiad Inequality Proofs
Zhaoqun Li"
Beishui Liao Zhejiang University baiseliaolzju. edu. en
Zhejiang University
Beijing Academy of Artificial Intelligence lizhaoqunozju. edu.
Qiwei Ye!
Beijing Academy of Artificial Intelligence quye@baai ac
Abstract
Mathematicians have long employed decomposition techniques to prove incquali- ties, yet automating this process remains a significant challenge in computational mathematics. We introduce IneqSearch, hybrid reasoning system that integrates symbolic computation with large language models (LLMs) to address this chal- lenge. InegSearch reformulates inequality proving structured search problem: identifying appropriate combinations of theorems that decompose expressions into non-negative components. The system combines symbolic solver for deductive reasoning with an LLM-based agent for constructive proof exploration, effectively implementing methodologies observed in formal mathematical practice. A key contribution of IneqSearch its iterative learning mechanism that systematically incorporates newly proven results into its theorem database, enabling knowledge acquisition during practice that enhances its capabilities without requiring hu- man intervention. In empirical evaluation on 437 Olympiad-level inequalities, IneqSearch successfully proves 342 problems, significantly outperforming existing methods and demonstrating the effectiveness of integrating symbolic and neural approaches for mathematical reasoning.
Introduction
Automating the proof of Olympiad-level inequalities in computational mathematics represents fundamental benchmark for evaluating the capabilities and boundaries of artificial general intel- Inequality proofs typically require both deductive inference and insightful transformations, making them valuable benchmarks for evaluating progress toward general-purpose mathematical reasoning. Recent approaches have made progress in mathematical reasoning through natural language proof generation using large language models (LLMs) [5] 6). formal proof tech- niques automated theorem proving (ATP) 7 [O] and mixed methods that combine these two strategies [2]. However, algebraic inequalities remain challenging, as they require constructing proofs within an infinite reasoning space.
ligence [1 3
To prove an inequality F 2 0, a common and effective strategy is to transform into a more manageable form by decomposing the original expression into tractable components. For instance, many proofs in Olympiad inequalities rely on intricate scaling techniques, which often employ
'This work was done during an internship at BAAI Corresponding author
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

or identity- rewritings. These techniques naturally lead to a decomposition of F. allowing to be expressed as sum of non non-negative components, namely F = Fi + F2 ..., where each F; 2 0. Inspired by this idea, we develop an automated approach that reformulates the proof of inequalities as search problem, aiming to decompose the target expression F into sum of known non-negative terms, i.e., F E, F.. Implementing this strategy in practice faces two critical challenges: (1) Inequality decomposition requires strong deductive reasoning to manipulate complex expressions. (2) Constructive proof's demand innovative strategies to adapt lemmas to specific problem structures.
auxiliary lemmas (e.g.,
To address these challenges, we introduce IneqSearch, a hybrid reasoning system that integrates sym- bolic computation with large language models, in which inequality proving is framed as an iterative search process. Specifically, leveraging the robust deductive capability of symbolic computation, we introduce a symbolic solver that formulates inequality proving as a search problem, enabling precise and systematic deductive reasoning. In parallel, an I.LM-based inductive agent is designed to explore constructive proofs, utilizing the inductive strengths of LLM to propose novel scaling techniques and transformations. A distinguishing feature of IneqSearch is its iterative learning mechanism, which autonomously incorporates solved inequalities into its knowledge base, continuously enhancing its proving capability and scalability to complex problems. This design reflects the cumulative nature of mathematical knowledge, where established results facilitate subsequent discoveries. Furthermore, IneqSearch ensures soundness by constructing verifiable proofs, and achieves interpretability through human-readable and transparent proving steps.
IneqSearch is evaluated on benchmark of 437 Olympiad-level inequalities, significantly outperform- ing leading methods. Notably, on the challenging MO-INT dataset [ our method achieves 100% success rate, demonstrating its effectiveness for particularly difficult cases.
2
Inequality Proving
We first formalize the inequality proving problem before introducing InegSearch.
2.1 Problem Formulation
Formally, inequality proving problem involves verifying non-negativity of an expression under specific conditions. For an inequality with n variables {2,} E IR", problem = (F, C) is defined by an inequality expression F( Fn. and condition expression C In), which can be formulated as:
(1) where ME {= We refer to F as the inequality and C as the assumption, where C may be absent if no additional condition is required. To focus on core mathematical proof techniques, we assume all variables are positive, cases involving negative values typically be proven in similar manner.
Prove that F(a1..... xx)) 2 O when C(zi. ba 0.
2.2 Decomposition-basse Proving
The fundamental methodology underlying our approach reformulates incquality proving as a decom- position task [3.. This approach is based on the principle that many complex inequalities can be systematically reduced to combinations of established non-negative expressions. We employ two methods for inequality decomposition (see Appendix for technical details):
Elementary Cyclic Polynomial Decomposition (ECPD) ECPD provides a systematic framework for representing and manipulating expressions in inequality proofs. An elementary cyclic polynomial of degree d in n variables can be expressed as
(()) k2.
km
CgC
where m & n and complex expressions into standardized forms, making them more amenable to systematic analysis. For example, we have:
k li + .... + km = d. This representation enables the transformation of
(n - 1) (c/"))² 2nc((n) 2 20, (c()))² 20(2) 30 2 0.

---

Solver S
Theorem Database T
Let au 0, 0, prove that:
3
La + +2++ Vilryt 8²2 2la)
TH
Preprocessing
Lige
TH
Σ rvy Σ
3
st 23
313
2
E ny.
220
7h
1/l 13)
Brys
Direct Proving
Scaling
7H
Proved
D 2p) Yagg:
ECPD
SOS
Inductive Agent M
TH
Engo
13 5r
Not Proved
TRio:
Search
Enge sle
wik
AAAAA
3+3
3 Σ
Σ
---1
1- +
Not Proved
X
Update
Proved
Logic System C
Figure Overview of the proving pipeline. The solver starts proving by processing the given problem into a standard format. Then theorem search identifies applicable theorems from the database and attempts decompose the inequality. If the proof fails, an inductive agent explores transformations to generate potential directions. If the proof succeeds, the logic system expands the theorem database by integrating newly proven results.
Sum of Squares (SOS) The SOS method provides a powerful certification mechanism for poly- nomial non-nege -ogatiiaty through quadratic decomposition. polynomial T( Fnn is an SOS polynomial if it can be expressed as T = Σ. t where each t; is real polynomial. For example, x² + 3² - 4ry + 2 (x² y²)² + 2(xy 1)² is sum of squares. In practice, finding an SOS decomposition is formulated as a semidefinite programming problem, enabling automated discovery of decompositions for complex polynomials.
The IneqSearch System
The development of IneqSearch is motivated by the observation that effective inequality proving requires both systematic deductive reasoning and constructive insight. The system architecture reflects this dual requirement, implementing a methodology that progresses from direct proof attempts to theorem-basee search, and finally exploration of problem transformations when simpler approaches are insufficient. As depicted in Figure [ IneqSearch is built upon proving pipeline that integrates symbolic computation, theorem search, and language model-guided exploration.
3.1 The Symbolic Solver
The symbolic solver S forms the deductive core of IneqSearch, enabling robust algebraic manipula- tions through preprocessing and theorem search.
Preprocessing Given problem (F, C²), solver first standardizes facilitate subsequent processing: (1) For homogeneous inequalities without explicit constraints, S introduces addi- tional normalization assumption Σ, x; (2) Fractional expressions are converted to equivalent numerator-only forms through algebraic manipulation. (3) The solver attempts to climinate radical

---

subexpressions in F using techniques analogous to unrad in SymPy; if unsuccessful, it retains the original form.
The preprocessing step ensures that the original problem systematically transformed into an equivalent and standardized form, making it suitable for subsequent procedures.
Theorem Search For simple problems, direct application ECPD or SOS methods often suffices.
When these approaches inadequate, IneqSearch implements more comprehensive search strategy. This search systematically examines possible representations of the target expression F as linear combination of established theorems from the database, effectively decomposing the original problem into previously solved components.
The theorem database T stores axioms and proven theorems in the form (g,, h.). indicating that 9i 2 0 under the assumption h2 = A direct corollary is that any non-negann non-negative linear combination of theorems is also non-negative:
Xig 20, Vi, h4 0A 2.
Given an inequality expression, the solver identifies applicable theorems, i.e. those for which h; = 0 satisfied, and formulates the search problem as follows:
Find d and Ji such that
F Σ Ash. 220, JEET.
where To= = 1 .kk....kk is the set of applicable theorems. The search problem corresponds to solving a system of equations for the coefficients (A,) To obtain a numerical solution, we formulate linear programming problem to determine feasible real values for { Specifically, the search problem feasible, S tries to find numerical solution where the coefficients { are non-negative and satisfy all the required constraints of the problem. When the entire search is successful, the inequality problem proven; otherwise, the proof fails.
k}
3.2 The Inductive Agent
For challenging problems where the symbolic solver fails, it may become necessary to rely on more sophisticated algebraic methods, including the adoption of widely used lemmas such as the Cauchy-Schwar inequality. We employ an LLM-based inductive agent M to explore constructive proof strategies. The agent analyzes the structure of the inequality and proposes transformations using well-known inequalities (such as AM-GM, Cauchy-Schwarz etc.) and homogenization, enabling further exploration. As illustrated in Figure 2 the exploration follows two directions: (1) Application of auxiliary inequalities to scale the original expression into more manageable forms. (2) Target shift by replacing constants based on given assumptions to achieve more homogeneous expressions.
For each difficult problem, given the infinite possibilities of constructive approaches, we ask M to provide multiple possible choices each step, and let S verify the validity of the explored scaling techniques.
Proof Construction Example Taking the case in Figure begins with S attempting direct methods, finding that neither ECPD nor SOS produces an immediate result. The system then queries its theorem database but fails to identify a suitable combination of existing results. Subsequently, the inductive agent analyzes the inequality structure and proposes several choices.
example, the solution process
For the left-hand side expression, M considers it suitable to adopt the Cauchy-Schward inequality, which states that (Ea)) 6²) > (Σab) ab) M then proposes two possible constructions by assigning b = Eeye x + yz and 1 E Eze aa=² + yz). For the right-hand side, which a constant, it can be rewritten using the assumption, enabling the original problem to reformulated in several equivalent forms. For example, A multiplies it by Eeyc x² or / Eeyye= x²/3. Using these transformations, the symbolic solver can attempt to prove total of additional inequality

---

LIIS
x² x²
Egye xt1
EErgo 22)2
Inequality Adaption
y
egee x² y
rayo xf 122
Cge
Let M, 2 such that x²
y²
a²
112
2
Prove that: 2² - yz
y²
+
22
Target Shift
3
E x²
E x² 2
eye
RHS
2
Figure 2: Exploration strategies utilizing the Cauchy-Schhi Schwarz inequality and homogenization. The exploration process proceeds in two directions: M adapts the inequality by transforming the left-hand side into multiple manageable forms, and rewrite the right-hand side into equivalent expressions that eliminate assumption.
Ecyy
3 Eaye x22/ under no assumptions. This completed proof is subsequently integrated into the theorem database, demonstrating how IneqSearch combines deductive verification with constructive exploration to expand its proving capabilities.
forms. Finally, S successfully proves Leye
3.3 The Self-improving Mechanism
distinguishing feature of IneqSearch its iterative learning capability that continuously expands the theorem database. As discussed earlier, the proving capability of IneqSearch is directly tied to the richness of the theorem database To enhance this capability, IneqSearch employs an iterative learning paradigm that continuously expands T by incorporating previously proven inequalities.
Logic System C During the proving process of problem P, C maintains set Sp containing all intermediate conclusions. After completion, proven theorems from Sp are selectively incorporated into T. For instance,
proof forms chain E₁ 2 0, E2 2 0, E. 2 O where (E, 2 0) (E.+1 2 0), each E; is analyzed and potentially added to the database. This ensures that every theorem in has been rigorously validated, guaranteeing the system's soundness.
Iterative Learning Initially, T contains only basic axioms (Appendix A.3 As IneqSearch solves problems, it progressively learns new theorems. This self-improving mechanism enables the system to tackle increasingly complex problems over time, each solved problem potentially provides new tools addressing more challenging cases.
3.4 Formal Proof Generation
prove:
Inequality (1 1/x)*(1 1/y)*(1 1/2) 64 >= Assumption
Simplify:a After simplification of numerator:
Inequality -64'xty*z (x 1)*(y + 1)*(2 1) >= 8, Assumption x x 8.
Transform:: Update after ECPD: Σxy 63*xyz 2, Eq(Ex, 1).
Method::
Search existing theorem set.
Result:: Proved theorem (TH_3) (TH_10): 63*xyz 2 (I)* 9*xyz) (2)*(1 27*xyz) >= 8.
Figure 3: Proof generated by IneqSearch.
The overall proof logic is straightforward to understand. It primarily involves algebraic transforma- tions and theorem search, systematically breaking down complex inequalities into manageable steps. The proof generation process mainly focuses on logging the procedure, including the transformations applied, the use of assumptions, and the theorems referenced during the proof. For instance, in

---

Table 1: Performance comparison of different models.
INEQ-437
MO-INT-20
Proof Type
Model
# Solved
Success Rate
# Solved
Success Rate
Gemini-2.0-Flash
62
14.2%
0
0%
Natural Language
DeepScek-RI
149
34.1% %
4
20%
OpenAl 03-mini
154
35.2%
15%
Semini-220-FFlan
0%
0%
DeepSeek-Provee Prover-V155
0.2%
0%
OpenAl o3-mini
2
0.5%
0
0%
Lean4
AIPS
10
50%
LIPS w/ 4o-mini
264
60.4%
18
90%
L.PSS w/ 03-mini
273
62.5%
18
90%
IneqSearch w/ 4o-mini
334
76.4%
19
95%
Formal
IneqSearch w/ 03-mini
342
78.3%
20
100%
Figure 3 each transformation step logged, providing clear and transparent explanation of the process.
Experimental Results
To evaluate the performance of our method, comparison of IneqSearch with baseline and state- of-the-art methods is presented, along with performance analysis of each component through an ablation study. The iterative progress analyzed to observe the system's 's self-improving capabilities. In the end, several case studies are provided for the visualization of IneqSearch's 's advantages.
4.1 Experimental Setup
We constructed INEQ -43,, benchmark of 437 Olympiad-level inequalities compiled from authoritative sources [4] 13 We included all problems expressible the form of Equation without manual selection, representing approximately 90% of inequalities these sources. The detailed content of the benchmark can be found in the supplementary materials.
Data Collection
Baselines We evaluated IneqSearch against leading LLMs (Gemini-2.OOFlashh 15), OpenAl o3- mini [66], DeepSeek-Provee Pronkk--rove---iiie [17.. DeepSeek-RI [8) and hybrid systems (AIPS M. LIPS (19)
both natural language and formal proofs. The temperature hyperparameter set 0.3 for all language models when applicable.
Evaluation For fair comparison, used three-shot setting in all comparison experiments. For natural language proofs, correctness was manually verified by experts. For formal proofs in Lean4, correctness automatically verified. We report the number of problems solved and the corresponding success rate for each dataset.
4.2
Main Results
Our experiments reveal a notable pattern: the integration of symbolic reasoning and neural approaches creates a system far more powerful than either approach alone. As shown in Table [ while state- of-the-art language models struggle with the precision required for inequality proofs, and symbolic methods alone lack creative problem-solving abilitics, IneqSearch combines the strengths of both worlds.
Analysis shows that the most powerful reasoning language model (o3-mini) solves only 35% and 15% of problems in INEQ-437 and MO-INT-20, respectfully, highlighting the limitations of purely neural approaches. Notably, language models demonstrate substantial difficulty in producing formal Lean4 proofs, with success rates below 1%. In contrast, IneqSearch achieves 78.3% success rate these challenging inequalities, demonstrating the effectiveness of the integrated approach in mathematical reasoning tasks. Hybrid methods like AIPS and LIPS show improved performance pure LLM

---

Table 2: Ablation study IneqSearch components.
ECPD
SOS
Target Shift
Exploration
Iterative Learning
Problems Solved
126
/
257
292
325
334
342
approaches but still fall short of IneqSearch's capabilities. By integrating inductive exploration with rigorous deduction, IneqSearch ensures both correctness and interpretability in its proofs. Detailed error analysis of LLM-generated proofs is provided in Appendix
Performance on High-Difffcuuly Problems IneqSearch shows strong performance problems that are difficult for existing methods. On the MO-INT-20 dataset, which contains real inequalities from Olympiad competitions, many problems require multi-step scaling and are often non-symmetric and non-homogeneous (see Appendix D). These characteristics pose significant challenges for symbolic solvers and LLMs.
First, symbolic solvers often failed to directly solve such problems. For example, the Polish-2004 problem requires the use of the Hölder inequality, while USAMO 2017 P6 involves the tangent line trick. Purely algebraic techniques, such as direct decomposition, rarely uncover these methods. Without such approaches, analyze the original expressions becomes extremely difficult.
Second, some problems require substantial algebraic manipulation and comparison. For instance, in IMO 2020 P2, even after applying the AM-GM inequality, the proof involves adding, subtracting, and comparing over thirty monomials. LLMs can often identify where AM-GM should be applied, but they usually cannot complete the subsequent deductive steps. In some cases, the models even doubts the correctness of its initial step.
These challenges persist even for state-of-the hybrid approaches. While other methods such as AIPS and LIPS are only able solve subset of the dataset, IneqSearch, in contrast, achieves full coverage by successfully proving all 20 problems.
4.3 Ablation Study
Table 2 presents systematic ablation analysis of IneqSearch's components, highlighting their individual contributions the system's performance. The baseline model, which uses only the symbolic solver, solves 257 problems. The integration of target shift for homogenization provides marginal improvement, solving 35 additional problems. The inclusion of LLM exploration further boosts performance, increasing the number of solved problems to 334. Finally, the iterative learning mechanism resolves 8 additional complex problems that were previously unsolved, achieving total of 342 problems solved. These results demonstrate the complementary nature of the system's 's components and the effectiveness of integrating symbolic and neural approaches.
4.4 Iterative Progress Analysis
The performance of IneqSearch demonstrates consistent improvement across multiple learning iterations. Figure quantiffess this progression, documenting increase from 257 successfully solved problems initially to 342 problems after multiple rounds of theorem acquisition and proof refinement. In each round, IneqSearch traverses the entire benchmark and attempts to prove each inequality within The theorem base will be updated once after completing the round, ensuring that any newly discovered results become available tools for subsequent iterations.
This iterative improvement follows a pattern consistent with incremental knowledge acquisition, where each round builds upon previously established results. By systematically incorporating new theorems into its proof, IneqSearch able unlock solutions to problems that were previously inaccessible. Figure illustrates a representative case of this process, where theorem T T'H estab-

---

Let M, 2 such that + y Prove that:
9
Rx:6
y2
16ryat) Lay
Eng
Mazyzj 23rgz + 2 )
120
16ry=(2 oy) Eey M(yy)) 23xya +1= (8) (TH H)) + (1) (TH.) (2) (THa.)) + (3) (THm.) (1) (THa) 2.
300
280
TH2 -Aryz Σ ay ((ry=) ayz
T
482ya Σ Σ sy 25rys
260
THu: Σ> zy 9rgs
TH
Σ Eay 9ayz
18(xy 22 + ys)
23
240
THis 27 ays
Axioms
Learned Theorem
Figure Visualization of cumulative problems solved across four rounds.
Figure IneqSearch successfully proves a hard problem leverag- ing previous proven inequality.
lished in earlier rounds, enables the solution of a previously unresolved inequality, exemplifying the practical benefit of cumulative learning.
The observed improvement pattern demonstrates the effectiveness of the system's knowledge accu- mulation mechanism, where each new theorem potentially extends the range of solvable problems. The continual expansion mathematical tools underlies the robust performance gains observed throughout the iterative process.
4.5 Computation Cost
IneqSearch first attempts to prove each incquality using the symbolic solver. If this attempt fails, the system proceeds to call the LLM for further cxploration. In our implementation, there are 5 inequality lemmas to be explored, and each inequality exploration calls the LLM once, with one additional retry if the first call is invalid. The exploration of inequality lemmas is conducted in parallel, allowing us to collect all possible valid scaled expressions after exploration.
Table 3 summarizes the average runtime and time budget for the proving steps of IneqSearch with 03-mini on our INEQ-437 benehmark. Only the major time-consuming steps are listed, and the steps are not strictly sequential in the implementation. Other routine algebraic manipulations are omitted, as their runtimes are comparatively negligible. The reported runtime for each process refers to the average time per single execution, although each process may be called multiple times within proof. For accurate measurement of actual solving time, we report the runtime for successful proofs, where InegSearch requires only 12.3 seconds average per problem, demonstrating high efficiency.
Table 4 presents the average solving time for successfully solved problems and compares our method to LIPS and o3-mini. Compared to LIPS, our approach achieves more than 100x speedup in runtime. While these results are convineing in practice, we note that this direct runtime comparison not entirely fair from algorithmic perspective, as the majority of the time cost in LIPS arises from repeated LIM calls. Our method is primarily solver-driven and typically requires far fewer L.LM calls per problem.

---

Table Runtime analysis (in seconds) the proof workflow on INEQ-437.
Module
Process
Avg. Runtime
Time Budget
ECPD Transform
0.6
30
Theorem Search
41.6
240
Solver
SOS
0.4
30
Total
12.3
300
Equality Condition
17.3
180
Target Shift
19.1
180
AM-GM Ineq. Expl.
32.6
180
Inductive Agent
Cauchy-Schwarz Ineq. Expl.
27.3
180
(o3-mini)
Hölder's Ineq. Expl.
41.0
180
Jensen's 's Ineq. Expl.
34.4
180
Tangent Line Ineq. Expl.
37.9
180
Total
65.8
300
Overall
24.1
900
Table Comparison of solving time (in seconds) and success rate.
Methods
Avg. Runtime
Success Rate
OpenAl o3-mini
63
35.2%
LIPS w/ 120 min budget
5187
62.5%
LIPS w/ 90 min budget
2946
50.3%
IneqSearch w/o LLM IneqSearch w/ 03-mini
12
66.8%
24
78.3%
4.6 Error Case in LLM's Output
Our analysis of LLM-ggnerated proofs reveals critical consistency issues, underscoring the necessity of formal verification in mathematical reasoning. When proving complex inequalities, LLMs are prone making subtle yet critical errors logical deductions or algebraic calculations. For example. in solving the inequality vor II+ + V6y + + v6z results in two attempts at calculating derivatives, as shown in Figure 6
3v3, Gemini2 produces contradictory
Such inconsistencies suggest that while LLMs mimic advanced mathematical reasoning, they require an automated verifier to ensure the correctness steps and prevent hallucinations, especially when solving problems that require rigorous deductive reasoning. Therefore, integrating rigorous verification mechanisms essential for both the reliability and trustworthiness of LL-M-assisted mathematical problem solving.
Attempt 2
Attempt
Let f(t) = /tt I. The first derivative
Let f(t) = vot 1. Then f'(t) 1/004I
given by f(())
(vot + = 2/0++1
voL+T
and (t) 3 (-1) (6r + 1)/3/2
vor+T 9(66 + 1)-3/2, Since (*(() < 0 for all t 0.
The second derivative is f((() $ (-1) (Gt + 1)-3/2 ("(() for O, the function f convex.
9(Gl + 1)
3/2 1//3/2 Since
f is concave.
Figure LLM generates inconsistent content in two attempts.
Discussion
IneqSearch implements critical principle for automated mathematical reasoning: continuously acquiring and applying mathematical knowledge. Its improved performance shows that effective reasoning relies on leveraging established results to construct new proofs, reflecting the cumulative nature of mathematics.

---

A promising research direction involves utilizing LLMs to extract generalizable patterns from specific problems. This approach aligns with established mathematical methodology: observation of patterns. formulation of conjectures, and subsequent verification. For example, consider the following IMO problem: for positive real numbers a, b, c, d such that ab + be + od + da 1, show de
that beotd ctd+a
6.3
d-a4b + m
a+b+c 2 3. This problem can be extended to a broader class of 1k2
inequalities, such as Σx s- [n-1)n where = Ej 24 and k2 = Eie, 2,2 The key insight is recognizing that denominators of the form x; and the cyclic condition ab + bc ed + da can be abstracted to the setting k.² = Σiej 2; representing an elementary symmetric polynomial of degree 2. Maintaining homogeneity during this abstraction process is essential. Such generalizations require pattern recognition and analytical reasoning capabilities well-suited LLMs' strengths.
6 Related Work
Our work integrates advances in mathematical reasoning, automated theorem proving, and Olympiad problem solving.
6.1
Mathematical Reasoning
Automated mathematical reasoning has progressed through several complementary approaches. Benchmarks like MATH [20] and GSM8K [2I] have established standards for evaluating reasoning capabilities. Advances in deep learning for symbolic mathematics [22] and automated theorem proving 223
24 25 have emerged through neural-guided proof assistants. Formal systems like 28 provide verification frameworks with extensive theorem libraries. Additional approaches include currieulum learning [29] and step-by-step verification (.. Despite these advances, inequality proving remains challenging due to its requirements for precise algebraic manipulation and problem-specific insights.
Lean 26
27
6.2 Olympiad Problem Solving
Recent innovations in automated Olympiad problem-solving include formal mathematics benchmarks like MiniF2F (7] and multimodal challenges in OlympiadBench [2]. Domain systems such as AlphaGeemetry [ have demonstrated success in plane geometry through learned construction of auxiliary elements. For inequality problems, LIPS 19 combines language models for expression rewriting with symbolic optimization tools, while AIPS [1] explores autonomous theorem genera- tion. Our work extends these approaches by implementing a systematic framework for inequality decomposition with iterative theorem acquisition, creating a self-improving system for mathematical reasoning.
Conclusion and Future Work
This work offers three main contributions: (1) it reformulates inequality proving theorem- based decomposition search, enabling the systematic breakdown of complex inequalities into manageable subproblems using established mathematical results; (2) it develops hybrid system that combines symbolic verification with LLMM-uided exploration, leveraging both rigorous algorithmic reasoning iterative learning
and the flexible problem-solving capabilities of L.MMs; and (3) it implements mechanism that continuously improves the system through ongoing theorem acquisition, allowing it expand its knowledge base and enhance its proving abilities over time. The effectiveness of this approach is demonstrated by the system's 's strong performance on challenging Olympiad inequalities, including complete coverage of the MO-INT-20 dataset.
Future work should extend this methodology to other mathematical domains and further enhance gen- eralization capabilities. The framework of decomposing complex problems, searching for established patterns, and incorporating new knowledge represents a generalizable approach to mathematical reasoning, with applications in formal verification and automated problem solving.
10

---

Acknowledgments
The research reported in this paper was partially supported by the National Social Science Foundation of China (20&2D047).
References
[1] Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without human demonstrations. The Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
[2] Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, Jie Liu, Lei Qi, Zhiyuan Liu, and Maosong Sun. OlympiadBench: A challenging benchmark for promoting AGI with olympiad-level bilingual multimodal scientific problems. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 2828-3850, 2024.
[3] Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 47744422) 2024.
[4] Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song. Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint ar arXiv:2402.033300 2024.
[5] Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, page 1229-1241 2023.
[6] Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce LLMs step-by-step without human annotations. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pages 9426 9439. Association for Computational Linguistics, 2024.
[7] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR, 2022.
[8] Zijian Wu, Suozhi Huang. Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internim2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700 2024.
[9] Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Dangi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07644. 2025.
[10] Kefan Dong and Tengyu Ma. Beyond limited data: Self-play Ilm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025.
[11] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In NeurlPS, 2022.
[12] Huaiyuan Ying. Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.0338 03847, 2024.
[13] Alijadallah Belabess, Advanced Olympiad Inequalities: Algebraic & Geometric Olympiad Inequalities. Independently Published, 2019.
[14] Zdravko Cvetkovski. Inequalities: theorems, techniques and selected problems. Springer Science & Business Media, 2012.
[15] Google Deepmind. Introducing gemini 2.0: our new model for the agentic era, December 2024.

---

[16] OpenAl. Introducing openai o3 and 04-mini, April 2025.
[17] Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. prepseek-prover-v// Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In ICLR, 2025.
[18] Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability in Ilms via reinforcement learning, arXiv preprini arXiv:2501. 2025.
[19] Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang. Kaiyu Yang, and Xiaoxing Ma. Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. In ICLR, 2025.
[20] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Proceedings of the Neural Information Processing Systems Track on Datasets and Bench- marks, 2021.
[21] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:21 14/68, 2021.
[22] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In ICLR, 2020.
[23] Stanislas Polu and Ily Sutskever, Generative language modeling for automated theorem proving. arXiv preprini arXiv:2009.033: 0333009900333,,... 2020.
[24] Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In NewrIPS, volume 35, pages 26337-2633 2022.
[25] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Mareus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In ICLR, 2024.
[26] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. page 625-635. Springer-Verlag, 2021.
[27] Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. LEGO-provee Neural theorem proving with growing libraries. In ICLR, 2024.
[28] Kaiyu Yang. Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. In NeurlPS, volume 36. 2024.
[29] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, arXiv preprini arXiv:2202.011344 2022.
[30] ForeverHaibara. Triple-sos. http:://ghhhhc...oooororaaaaaaap 2025.
12

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: See Abstract and Introduction.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how be expected to generalize other settings.
much the results
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
See Appendix Limitation.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification. asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low images are taken in low lighting. Or speech-to-text system might be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach address problems of privacy and faimess.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question:
For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
13

---

Justification:
All theorems stated are either from established literature or are provided with accompanying proofs.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proof's can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: See Experimental Results.
Guidelines:
The answer NA means that the paper does include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome deseribe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
14

---

Answer:
[No]
Justification:
The data is provided. The code is not yet ready for publication.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
/ ccpppi.ccppulli//uuuii wwwpc//ggue////eeeeeoooc CoodeSubeiiieeee ssi wswonnolli onnolicy)))) for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification:
See Experimental Results.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification:
We use n-short settings in experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, at least for the experiments that support main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
should be clear whether the error bar is the standard deviation the standard error of the mean.
15

---

It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of enrors is not verified.
For asymmetric distributions, the authors should be careful to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative eтror rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of exccution) needed to reproduce the experiments?
Question:
Answer: [No]
Justification: No GPU was used in the experiments. All computations can be executed on a standard personal computer.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics htttp::/neeurps http:///wwaapcccpoooooccccccaaaa
Answer: [Yes]
Justification:
Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g.. if there is special consid- cration due to laws or regulations their jurisdiction..
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
16

---

The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Lieenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
17

---

If this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification:
See supplementary materials.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/mmoel as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question:
Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
18

---

Question: Does the paper describe the usage of LLMs if it is important, original, or non-standard component of the core methods this research? Note that if the LLM used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Answer: [Yes]
Justification: LLM usage is declared.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs any important, original, non-standard components.
Please refer to our LLM policy fattps://neurip::: httpaarrpp...coooofffeeee/e////s for what should or should not be described.
19

---

Appendix
A Proof Methodologies
A.1 Elementary Cyclic Polynomial Decomposition
Elementary Cyclic Polynomial Decomposition (ECPD) is calculation- approach designed for proving cyclic inequalities. This method enables us to leverage computational tools and to build unified-format format theorem library for addressing complex algebraic inequalities, extending beyond cyclic cases alone.
A fundamental principle in algebraic inequality theory is that the structure of the sayynommal--hhhhhe symmetric or merely eyclic-determinn determines the most suitable basis for its decomposition and analysis.
Theorem 1. Let T(11, T2..... . .n) be symmetric polynomial in variables. Then T always be expressed as a polynomial in terms of the elementary symmetric polynomials S1, S2,..., iag....,,, Sa. where
S
34i S
E IStCJEn
S. 21 ...2....0
This classical result allows for the reduction of symmetric inequalities expressions involving only the elementary symmetric polynomials. Such a reduction significantly simplifies both theoretical analysis and computational verification, the search space for potential equalities or extreme cases is greatly narrowed.
For polynomials exhibiting cyclic symmetry, parallel decomposition exists, which forms the backbone of the ECPD method:
Theorem Let T111, T2,..., ,n) be cyclic polynomial of in n variables. Then T can always be expressed as polynomial in terms of the elementary cyclic polynomials ko......kk where
(x)
(n)
Σ cye
k2
Kam
with m S n and kn + li +....
ki deg
The introduction of the elementary cyclic basis enables systematic treatment of cyclic inequalities, especially when the expressions are not fully symmetric. By expressing any cyclic polynomial in this basis, unlock the potential for automated computation and algorithmic proof strategies, well as a unified language for theorems and results.
A.2 Sum of Squares
One of the fundamental procedures for proving inequalities is to rewrite them as sum of squares, thereby establishing the non-negativity given expression. This property forms the foundation of the SOS method.
Theorem (Hilbert). Ler T(11, , .,,) be polynomial.
IfT 2 and is homogeneous, then can be expressed as
T
Σ k
where lg certain real rational functions.
T 0 and is non-homogeneous, and {z, Yim satisfies the condition Σ xs S 1, then T can be expressed as
an+1
T
Σ Ck x 02 ...IT
On
1
Σ
where 1 are non-negative integers and 0.
20

---

These theorems are qualitative results that help establish the existence of a method to prove that a polynomial is non-negative. For homogeneous functions, this is achieved by analyzing sums of squares, while for non-homogeneous functions, it involves expressing the polynomial as sum of non-negative quantities. In 30. this principle implemented based on an explicit semidefinite program.
SDPSOS Given real polynomial T( .... vn), together with inequality constraints gi (z) > O,..., (x) 2 0 and equality constraints hi (ar) = -..... (x) = O. the SDPSOS method seeks to certify nonnegativity of T under these constraints by constructing SOS representation:
T(x) Σ s; (1()) + Σ h,()),
where (z) := 1, each (z) is an SOS polynomial, and (z))) are arbitrary polynomials. Each SOS term can he written as (z) = (1(x)) Ma), where M; is symmetric positive semidefinite matrix and (2)) is the vector of monomial basis elements up a prescribed degree.
Thus, certifying nonnegativity reduces to finding matrices Mg, MI...., Mr = 0 and polynomials & (xx) such that
T(x) = Σ
(z) + Σ tz)()))))))
with all coefficients matching when both sides expanded. The entries of the Gram matrices M, and the coefficients of (z)) become variables in a system of linear equations, while the positive semidefiniteness of M, is imposed as semidefinite constraint.
Therefore, the problem of certifying nonnegativity via SOS reduces to the following explicit semidef- inite program (SDP):
Find symmelric matrices Mo, Mi,..., Mr and polynomials i (x),..., (xx) such that
& T(x) = 1 (1) (2.(z)
Σ h((x)
1=
subject to M, 2 0, i= k.....
This modeling is possible because the set of all positive semidefinite matrices forms and the set of solutions to the linear equations is an affine subspace; their intersection is convex set. Therefore, the problem becomes convex optimization problem with linear equality constraints and matrix positivity constraints. I(x) and the constraints exhibit symmetry, equivalent terms under the symmetry group can identified, reducing the size of the SDP. Additionally, if T(x) vanishes certain points (equality cases), the corresponding Gram matrices are further constrained to have these directions in their kernel, reflecting additional algebraic structure.
cone,
A.3 Axioms in Theorem Database
IneqSearch is designed to evolve from basic problem-sole solving capabilities to an advanced level of expertise through continuous learning and adaptation. Initially, the theorem database contains a set of fundamental theorems from Murihead's inequality, Shur's inequality and Vasc's inequality, which serve axioms.
Theorem 4 (Muirhead's Inequality). Let 3i, .2....,,T,
Tn be non non-negative real numbers, and let (a.,..., an) and b (b),..., b,) be two sequences of non-negative integers in non-increasing order. If a majorizes b, that is,
Σ
Σa
6
by for all 1 < k < n,
and
Σ i=1
aj
di
==1
then the following inequality holds:
Σ
az(1) (z(2)
ae(n)
Σ
bo()) ba(a)
be(n)
I1
x22
Fn
X2
En
oES
oeS..
21

---

where Sn, denotes the set of all permutations on elements.
In this work, we develop an automated pipeline for the systematic generation Muirhead-tye -ypp inequalities. Given the number of variables n and the total degree d. the algorithm enumerates all possible integer partitions (01, 02, ................................ Qn) non-increasing order with d1 + +... an d. For each pair of partitions (a, b) such that majorizes b, the corresponding difference of symmetric sums is constructed:
Σ oES
Po(t) 11
(m(()
Σ oES
(e(l) 1
Po(n)
Each inequality is then canonicalized by factoring and removing any constant multipliers. To ensure minimality, the collection is further filtered to eliminate redundant inequalities via numerical evaluation and linear dependence checks.
B
Inductive Agent Configuration
B.1
Prompt Template
Here, we present the prompt template used to automate the application of the Cauchy-Schwar inequality with the LLM. Other exploration prompts are similar and we will include them at the revised version.
Prompt for Souchy-Schwarz Inequality Exploration
We solving inequality problem. Please do not the code interpreter.
The inequality is: (S_str)
We have the following important information:
1. Equality holds for: [cond_stt str)
2. Assumption condition: [assump_ste str)
Now, we want to use the Cauchy-Schwarz Schwarz incquality to scale S, so that we can obtain an expression which is casier to handle. The term indices are: (term_dict) Recall that the Cauchy-Schwarr inequality is:
(E A. B,) 2 (E C.)² or Σ C. VEL AJE B.). where C, = VA,BB
Follow these steps to determine whether the original incquality is suitable for applying the SuuchySSchwarz
inequality:
Identify the terms that are suitable for Cauchy-Schwarz inequality, and return their term indices.
2. Determine the role of these terms as A; or C, based on their coefficients: A; for positive, C, for negative.
(1) If the role is A., use the first form of the given Cauchy-Schwee Schwarz inequality; otherwise, use the second.
(2) Ensure that the role (A; or C.) included among the terms of S.
Design B; that other role (A, or C.) easy handle.
4. If the Cauchy Schwarz inequality is applicable, return the corresponding term indices as list of integers.
Provide your analysis and calculation steps, and summarize your answer in JSON. The JSON format begins with jsoonn shown below. Each term should be LaTeX string without the $ symbol, and the product sign should explicitly written between parentheses in expressions: jsson
"applicable": true or false, "role": "A_i" "C_i". "term_ nerm__numers": [numl, num2, ...] corresponding to the indices of A1/C1, A2/C2... "B 1": latex formula corresponding to A₁ or C1, "B_2": latex formula corresponding to A2 C2,
For each input inequality, we decompose it into individual algebraic terms, assign each term unique index, and represent them in LaTeX format as a dictionary (term_dict). For example, for the inequality a² + 1/2 + c² 2 ab + be + ca, the term_ term_dict dict would be [1: "a^2", 2: "bΛ2", 3: "c^2", "-ab", "-be", 6: "-ca"". We also provide the equality condition (cond_ste _srrr)) and the assumptions (assump_ae _str as LaTeX strings in the prompt, ensuring the model has access to all
22

---

relevant information during reasoning. The prompt instructs the model to analyze the structure of each term determine its role the Sauchy-Schware inequality as either A, Ci. and systematically design the corresponding B; for each.
B.2 Post-processing
In the model response, we extract the relevant terms from term_dict according to the term_net carme_n in the JSON, and combine them with the extracted B; expressions to automati- cally assemble standard Cauchy-Schwand inequality. For example, if the role is As, we construct
2
Σ 4.
Σ Bi 2 EVA.B.
Any error encountered during this construction process (as detected by our multiple symbolic checks) regarded exploration failure.
C
Limitation
Theorem search method equipped with ECPD and SOS is theoretically capable of solving all inequality problems within Equation[] However, in practice, the search process is often challenging. Our methodology relies on the decomposition identity = >.F. Fi. where a necessary condition for a successful search that the equality conditions must be satisfied for all subcomponents:
Suppose x = (I1,
En) such that F(x) = O.
Then for every i, from (x 2 0. have Fx 0.
For many hard inequalities, the equality conditions are uncommon may not exist in R+, necessitat- ing case-by-case analysis. For example, consider proving the inequality 12(E x² x² eye x²) S Enye xy under the assumption x + + z = 1. The equality holds and only if (x, y, =) = (0,0, up to permutation. Then all theorems g for which g(0, 0, 1) * O will not be applicable.
Such cases demonstrate that equality conditions can be highly restrictive. Consequently, if there are not enough applicable theorems with this equality condition in the database, it will limit the applicability and effectiveness of the search in practice.
D Additional Examples
Here are some examples drawn from MO-INT-20 dataset [ for our method illustration.
IMO 1990 Shortlist
For a > 0, b > 0, c > 0, d > 0 such that ab + be + cd + da = 1, show that:
²² + + ctd+a d +
a
b
d3 1
2
atb+c
Poland 2004:
For > c 0, d > show that:
b
d
3a3 + 63bcd) 1 (63acd + b2)s (63add + co) (63abc da)s 2
USAMO 2017 P6:
For a 2 0, 2 0, e 0, d 2 0 such that a + b d = 4, show that:
a b
c
d 2
+
a +4 2 3
b3 + 4
c +4
d +4
IMO 2020 P2:
For a 2 b, b c, c2 d, d > such that a + b c + d = 1, show that:
(a 26 3c 4d)a o'd < 1
23

---

E LLM Proof Generation
For the Lean4 code generation task, each problem initially translated into Lean4 code using fixed template. The LLMs are then prompted to complete the code. One example Lean4 code is:
import Mathlib
theorem inequality_probll
(x y R)
(hx x > 0) (hy : y > 0) (hz > 0) (cond x +
y + z 1):
(1 1 x) * (1 + 1 / y) (1 z) 2 64 by
The corresponding response of ol-mini is provided below.
import Mathlib
theorem inequality.probler
(x z R)
(hx > 0)
(hy y > 0) (hz 0) (cond : x y + z = 1) :
(1 1/x) * (1 + 1/y) * (1 1/2)
64: by
have h_sym : x = y A y
:=
by
let f := x (x y 2 : :)
(1 1/x) * (1 + 1/y) (1 1/2)
sorry
cases h_sym with hxy hyz subst hxy
subst hyz
have h_val : x = 1/3 : by
rw [ond at hyz linarith
rw h_val simp norm_num
exact le_refl 64
Based the messages from the Lean4 server, the code contains several errors. These errors include an Invalid Pattern caused by the use of an improper constructor, Unsolved Goals due to the lack of proof for the symmetry assumption (r y y = 2), and an Unexpected Token error arising from the use of * instead of a valid logical operator. These issues indicate issues with pattern matching, incomplete proofs, and syntax within the code.
Our analysis of the outputs for several problems reveals frequent errors, such as confusion between Lean3 and Lean4 syntax, including the misuse of begin and Real sq__nnneg. For more complex problems, the models often fail to perform even basic logical reasoning during code generation.
In the natural language testing setup, problems are presented in LaTeX format, and L.MSs are tasked directly with generating proofs. The proof produced by ol ol-mini is presented in Figure 7 which successfully solves the problem.
24

---

To prove that for positive real numbers 2, y, satisfying xr + + 1. the inequality
[ (1+
1 xt
1
1 y
1
1
64
holds, we use Jensen's Inequality with a convex function.
Key Steps
Rewrite the product as:
(1+
1
(1+
1
y +1
++1
1+
8
x
3/
2. Take natural logarithms:
In
(
(1+
1
1 b)
In 1+
1
In
1 y
!
In 1+ (1+1)
Use the convex function f(t)
(1 !). whose second derivative (t)
1241 > 0, to apply Jensen's
Inequality:
(1 + !) In (1+ :) + +In (1+1)
3) :)
2
1
IIn(4)
3
4. Multiply by 3 and exponentiate:
In (1+ 2
In644) = (1+ 1
1+ 1
(1+
2 64
y
Conclusion
Equality holds when y === satisfying + y + 1. Thus:
1 1 = -
1 +
-
2
64
2
for all n. U, >> with + 2
Figure 7: Natural language proof of ol-mini. correctly adopts Jensen's Inequality and successfully solves the problem.
25


Reviews:
[{"review_id": "HwlLeEurBu", "reviewer": "Reviewer_ZztM", "summary": "The paper introduces IneqSearch, a hybrid system for proving Olympiad-level algebraic inequalities. A symbolic solver first tries direct decompositions and searches a growing theorem database; when that fails, an LLM-based “inductive agent” suggests transformations. Successfully proven sub-results are fed back into the database so the system “learns” over multiple passes. On the authors’ new INEQ-437 benchmark and the MO-INT-20 set, IneqSearch solves 342/437 (78 %) and 20/20 (100 %) inequalities, substantially outperforming state-of-the-art LLMs and prior hybrids such as LIPS and AIPS. The system outputs human-readable proof logs and formal Lean 4 certificates.", "questions": "1. How does IneqSearch perform on publicly used inequality suites such as IneqMath? [Sheng et al., 2025] \n2. Could you quantify IneqSearch’s compute footprint (e.g., wall-clock time per problem, total GPU/CPU hours, number of LLM calls) and compare it directly to the baselines you evaluate against (LIPS, AIPS, pure-LLM solvers)?\n3. Can you provide more details on INEQ-437's construction (e.g., difficulty distribution)?", "limitations": "Partially addressed - the paper contains a dedicated “Limitations” appendix, but it skips compute-resource discussion and omits the lack of external benchmarks; these should be added. Otherwise the section is adequate.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\n* Strong empirical results \n* The system has a notion of memory (theorem database) which allows for self-improvement\n\nWeaknesses:\n*  Evaluation is almost entirely on an in-house benchmark created by the authors (except MO-INT-20 which is a small set); external sets such as IneqMath are missing. \n* Heavy reliance on hand-crafted ECPD/SOS + linear programming - may not generalise.\n* Domain scope is narrow (inequality problems)\n* The approach doesn't make proper use of stronger LLMs (the improvement from 4o-mini to o3-mini is marginal)", "was_revised": true, "final_justification": "The authors have addressed my concerns by reporting competitive scores on IneqMath benchmark, also updated the manuscript with compute efficiency metrics and more details about the dataset. I believe this strengthens the paper by providing more external evaluation and runtime metrics, which allows for fair comparison with other methods. The method performs well in these comparison, and therefore I raised my score.", "rebuttal": "Thanks for your review.\n\nEven though DeepMind recently used Gemini (with natural language) to win a gold medal in the IMO, our results show that LLMs still face significant limitations in Olympiad inequality proofs. Algebraic inequality proving is exceptionally challenging because it involves navigating an infinite reasoning space and requires both rigorous deductive reasoning and constructive proof techniques. Combining symbolic computation with LLMs enables two complementary modes of thought—rigorous deduction and creative exploration—making this hybrid approach especially powerful for tackling inequalities.\n\n# Takeaways\n\n1. Relying solely on LLMs to generate natural or formal proofs remains challenging. Our work demonstrates that integrating symbolic solvers with LLMs enables hybrid reasoning, resulting in substantial performance improvements. T\n\n2. The decomposition and search framework offers a promising direction for automated inequality proving. By leveraging LLMs for implementation within this framework, our results establish a practical path forward for general automated inequality proving.\n\n\n# Question response\n## Question 1\nIneqMath is a benchmark designed to test LLMs on inequality problems, rather than focusing solely on proving inequalities. Many problems cannot be directly transformed into proof statements. For example, some require demonstrating that an inequality does not hold by providing a numerical counter-example. For evaluation, we used the dev split, which contains 100 problems in total. Among them, we manually determined that 68 problems can be converted into proof problems.  IneqSearch successfully proved 48 of these, resulting in a success rate of 70.6\\%.\n\n## Question 2\n**Table 3.** Runtime analysis of the proof workflow on INEQ-437.\n| Module                    | Process                      | Avg. Runtime (s) | Time Budget (s) |\n|---------------------------|------------------------------|------------------|-----------------|\n|                           | ECPD Transform               | 0.6              | 30              |\n|                           | Theorem Search               | 41.6             | 240             |\n|                           | SOS                          | 0.4              | 30              |\n| Solver                    | **Total**                    | **12.3**         | **300**         |\n|                           |                              |                  |                 |\n|                           | Equality Condition           | 17.3             | 180             |\n|                           | Target Shift                 | 19.1             | 180             |\n|                           | AM-GM Ineq. Expl.            | 32.6             | 180             |\n|                           | Cauchy-Schwarz Ineq. Expl.   | 27.3             | 180             |\n|                           | Hölder's Ineq. Expl.         | 41.0             | 180             |\n|                           | Jensen's Ineq. Expl.         | 34.4             | 180             |\n|                           | Tangent Line Ineq. Expl.     | 37.9             | 180             |\n| Inductive Agent (o3-mini) | **Total**                    | **65.8**         | **300**         |\n|                           |                              |                  |                 |\n| **Overall**               |                              | **24.1**         | **900**         |\n\n---\n\n\n**Table 4.** Comparison of solving time and success rate.\n| Methods                  | Avg. Runtime (s) | Success Rate |\n|--------------------------|------------------|--------------|\n| OpenAI o3-mini           | 63               | 35.2%        |\n| LIPS w/ 120 min budget   | 5187             | 62.5%        |\n| LIPS w/ 90 min budget    | 2946             | 50.3%        |\n| IneqSearch w/o LLM       | 12               | 66.8%        |\n| IneqSearch w/ o3-mini    | 24               | 78.3%        |\n\n\n---\n\nIneqSearch first attempts to prove each inequality using the symbolic solver. If this attempt fails, the system proceeds to call the LLM for further exploration. In our implementation, there are 5 inequality lemmas to be explored, and each inequality exploration calls the LLM once, with one additional retry if the first call is invalid. The exploration of inequality lemmas is conducted in parallel, allowing us to collect all possible valid scaled expressions after exploration.\n\nTable 3 summarizes the average runtime and time budget for the proving steps of IneqSearch with o3-mini on our INEQ-437 benchmark. Only the major time-consuming steps are listed, and the steps are not strictly sequential in the implementation. The reported runtime for each process refers to the average time per single execution, although each process may be called multiple times within a proof. For accurate measurement of actual solving time, we report the runtime for successful proofs, where IneqSearch requires only 12.3 seconds on average per problem, demonstrating **high efficiency**.\n\nTable 4 presents the average solving time for successfully solved problems and compares our method to LIPS and o3-mini. Compared to LIPS, our approach achieves more than a 100× speedup in runtime. While these results are convincing in practice, we note that this direct runtime comparison is not entirely fair from an algorithmic perspective, as the majority of the time cost in LIPS arises from repeated LLM calls. Our method is primarily solver-driven and typically requires far fewer LLM calls per problem.\n\n\n## Question 3\nSince our benchmark does not contain any human annotations such as the number of steps, problem difficulty becomes hard to formally define. From the perspective of IneqSearch, those inequalities that can be proved by the solver at the very beginning are considered relatively easy samples (see Ablation Study). To provide a more intuitive description of the difficult cases in the benchmark, we instead analyze the failed cases to better reflect the types of challenging problems encountered by IneqSearch.\n\n### Uncommon Equality Conditions\nAs discussed in the Limitation section of the Appendix, a necessary condition for a successful search $F = \\sum_i F_i$ is that all equality cases must be satisfied for each $F_i$. Some problems, however, have uncommon equality conditions. For example,\n\n$$\n\\frac{256}{3125} \\geq x z^4 + x^4 y + y^4 z\n$$\n\nwith $x + y + z = 1$ attains equality when $(x, y, z) = (4/5, 1/5, 0)$ under cyclic permutation. Another illustrative example is\n\n$$\n\\frac{1}{81} \\geq \\frac{xyz}{(x+1)(x+y)(y+z)(z+16)},\n$$\n\nwhere equality holds at $(x, y, z) = (2, 4, 8)$. \n\nSolving such problems often requires more sophisticated, constructive algebraic proofs.\n\n\n### Non-directly Usable Assumptions\nA significant proportion of problems involve assumptions that are either non-standard or couple the variables in ways that prevent direct normalization or substitution techniques. For example, constraints such as\n\n$$\n\\frac{1}{x+1} + \\frac{1}{y+1} + \\frac{1}{z+1} = 2\n$$\n\nor\n\n$$\nx + y + z + 1 = 4xyz\n$$\n\nmake it challenging for solvers to apply classical inequality lemmas directly.\n\nThe key to addressing such problems often lies in transforming the given condition into a more manageable form, rather than directly substituting it into the inequality.\n\n### Non-homogeneity\nIneqSearch relies on homogeneity information to decompose inequalities. However, the majority of unsolved inequalities in this benchmark are non-homogeneous.\n\nFor example, consider\n\n$$\n8 + 2x^2 + 2y^2 + 2z^2 + xyz \\geq 5x + 5y + 5z,\n$$\n\nwhere the left-hand side contains constant, quadratic, and cubic terms, while the right-hand side is purely linear. The lack of a uniform degree structure complicates both analytic and algorithmic approaches.\n\nSuch non-homogeneous structures often arise from the underlying construction of inequalities involving constants, such as the simple case $x^2 - 2x + 1 \\geq 0$, which contains non-homogeneous terms. The algebraic construction involving constant terms remains a significant obstacle for our symbolic solvers.\n\n# Concern about limited domain\nWe claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its **scalability** in design.  \n\n**Decomposition and search** are our foundational principles, with neuro-symbolic integration and self-improvement as features that can be extended to general inequality proving. This principle is not limited to proving only polynomial or rational function inequalities, but can be generalized to a wide range of inequalities beyond the current scope of Olympiad-style problems. For example, our decomposition approach closely resembles the methodology for solving linear matrix inequalities, supporting the generalization of our framework to this area, potentially with advanced algorithms such as PIETOOLS.  \nTo further illustrate this potential, let us consider an example of an integral inequality—an area we are actively investigating as a promising direction for future work.\n\nLet  $f(0) = 0$, $f(x) \\in C^1[0,1] $. Consider the integral inequality\n\n$$\n\\int_0^1 (5 - x^2) f'(x)^2\\,dx \\geq (\\pi^2 + 2) \\int_0^1 f(x)^2\\,dx\n$$\n\nwhich can be established via SOS:\n\n$$\nLHS-RHS=4\\int_0^1 \\left( f'(x) - \\frac{\\pi f(x)}{2\\tan\\frac{\\pi x}{2}} \\right)^2 dx+ \\int_0^1 (1-x^2) \\left( f'(x) - \\frac{f(x)}{x} \\right)^2 dx \\geq 0\n$$\n\nFinally, we wish to avoid making overreaching claims that our method will fundamentally advance general mathematical reasoning or development, as mathematical reasoning itself is both profound and extensive.  Nonetheless, we emphasize that **algebraic inequality proving** remains a vast and essential domain, with frequent applications in mathematics and theoretical physics."}, {"review_id": "F7nGTSZ9Cd", "reviewer": "Reviewer_eiiF", "summary": "The paper introduce IneqSearch, a neuro-symbolic system, automates the proof of Olympiad inequalities using symbolic computation and LLM-based heuristic construction. The system decomposes the target inequality into a sum of non-negative expressions, which are either established theorems in a database or constructed by LLMs. Proved inequalities are then added to the database, leading to a self-improving system. The system’s performance is evaluated on two datasets, demonstrating its significant superiority over existing baselines.", "questions": "- It is unclear to me how the generated proofs are verified. Does IneqSearch generate proofs in Lean4?\n- In the evaluation, other methods for comparison are evaluated for three shots. How does it count for one shot? For example, in LIPS, each attempt is allocated 90 minutes. Does one shot of LIPS take 90 minutes in the evaluation?", "limitations": "While the details of the agent design are absent, the potential application of paper is limited to automated inequality proving.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n+ The task of proving Olympiad inequalities addressed by the paper is challenging.\n+ The proposed approach is mathematically well-founded.\n+ The paper collects a large dataset of Olympiad inequalities, which is valuable for further development.\n+ The performance of the experiment is impressive, significantly surpassing existing baselines.\n\nWeaknesses:\n- The design of the LLM-based inductive agent is not adequately presented. Given that the agent is a crucial component of this neuro-symbolic system, the paper should provide more detailed information about the agent, including the prompt and some example inputs.\n- In addition to the absence of agent information, the paper requires further justification for the design of the agent. As evidenced in Table 2, the performance of the symbolic component alone is already impressive. The combination of ECPD and SOS effectively resolves 257 problems, closely approximating the performance of LIPS, which addresses 273 problems. Without additional justification, it appears that the majority of the improvement is attributed to the symbolic component, which is limited to inequality proving problems. As a result, its influence on broader neuro-symbolic systems may be reduced.", "was_revised": true, "final_justification": "The authors have provided sufficient technical details, including the verification process and agent configuration, which strengthen the credibility of their contribution. However, the proposed techniques appear to be narrowly tailored to the inequality proving, limiting their generalizability to broader applications. As such, while the work is technically sound, its overall impact may be constrained by its limited scope.", "rebuttal": "Thanks for your review.\n\nEven though DeepMind recently used Gemini (with natural language) to win a gold medal in the IMO, our results show that LLMs still face significant limitations in Olympiad inequality proofs. Algebraic inequality proving is exceptionally challenging because it involves navigating an infinite reasoning space and requires both rigorous deductive reasoning and constructive proof techniques. Combining symbolic computation with LLMs enables two complementary modes of thought—rigorous deduction and creative exploration—making this hybrid approach especially powerful for tackling inequalities.\n\n# Takeaways\n\n1. Relying solely on LLMs to generate natural or formal proofs remains challenging. Our work demonstrates that integrating symbolic solvers with LLMs enables hybrid reasoning, resulting in substantial performance improvements. T\n\n2. The decomposition and search framework offers a promising direction for automated inequality proving. By leveraging LLMs for implementation within this framework, our results establish a practical path forward for general automated inequality proving.\n\n# Question response\n## Question 1\nIneqSearch generates **pure algebraic proofs**, whose soundness can be guaranteed and verified by symbolic computation engines. While our proofs are not formally verified by an axiomatic logic system, they are validated through explicit algebraic computation. Advanced numerical algorithms (such as SOS) ultimately produce symbolic proofs, ensuring that the numerical process does not affect the algebraic correctness of the final result. Our implementation is based on SymPy and Mathematica; below we provide a detailed explanation.\n\nGiven an input expression $F$ to IneqSearch, all possible algebraic manipulations can be divided into three categories:\n\n- **Rewriting**: $F = \\sum_i F_i$, including ECPD transformations, SOS, theorem search, etc.\n- **Inequality Transformation**: $F \\geq 0 \\Leftrightarrow G \\geq 0$, including removing denominators, removing radicals, etc.\n- **Scaling**: $F \\geq G$, used only during LLM exploration.\n\nThe first two types of manipulations are mathematically equivalent.\n\nThe third operation, scaling, is carefully constrained to ensure correctness. For example, when instructing the LLM to apply the Cauchy-Schwarz inequality, $(\\sum A^2)(\\sum B^2) \\geq (\\sum AB)^2$, we directly provide $A$ according to the specific problem and let the LLM construct $B$. Regardless of the choice of $B$, the resulting scaling **always preserves validity**, though it may introduce over-scaling. This procedure is conceptually similar to constructing `tactics` in Lean, as implemented in LIPS.\n\nTo enhance the reliability of our implementation, we employ both symbolic and numerical checks.\n\nFor the final algebraic proof $F \\geq \\sum F_i$, if there is no scaling, _i.e._, the LLM is not involved and $F = \\sum F_i$, we directly verify the equality by symbolic computation. In our approach, each $F_i$ is either a square or a previously established theorem, both of which are non-negative, so the overall proof is guaranteed to be correct. If scaling is involved, we additionally verify that the inequality construction is correct by including assertion statements to ensure symbolic correctness during the construction process.\n\nAdditionally, after removing denominators or radicals, or when scaling occurs, we perform numerical verification by sampling variable values. While not mathematically necessary, this step serves as an extra safeguard against potential implementation errors.\n\n## Question 2 \nFor LLM natural language proofs, we queried the LLM three times for each problem, generating three independent responses. If any one of these responses was correct, we considered the attempt successful. For LIPS, if it exceeded the time budget or the maximum number of iterations, the attempt was marked as failed. \nSimilarly, we performed three independent runs of LIPS and considered a problem solved if at least one run succeeded.\n\n\n# Concerns\n## Inductive Agent Configuration\n#### Prompt Template\n\nHere, we present the prompt template used to automate the application of the Cauchy-Schwarz inequality with the LLM.  \nOther exploration prompts are similar and will be included in the revised version.\n\n**Prompt for Cauchy-Schwarz Inequality Exploration**  \n>\n> We are solving an inequality problem. Please do not use the code interpreter.  \n>\n> The inequality is:  \n> `{S_str}`\n>\n> We have the following important information:\n>\n> 1. Equality holds for: `{cond_str}`\n> 2. Assumption condition: `{assump_str}`\n>\n> Now, we want to use the Cauchy-Schwarz inequality to scale $S$, so that we can obtain an expression which is easier to handle.  \n> The term indices are:  \n> `{term_dict}`\n>\n> Recall that the Cauchy-Schwarz inequality is:\n>\n> $$\n> \\left(\\sum_{i=1}^n A_i\\right) \\left(\\sum_{i=1}^n B_i\\right) \\geq \\left(\\sum_{i=1}^n C_i\\right)^2\n> $$\n>\n> or\n>\n> $$\n> \\sum_{i=1}^n C_i \\leq \\sqrt{\\left(\\sum_{i=1}^n A_i\\right) \\left(\\sum_{i=1}^n B_i\\right)},\n> $$\n>\n> where $C_i = \\sqrt{A_i B_i}$\n>\n> **Instructions:**\n>\n> 1. Identify the terms that are suitable for the Cauchy-Schwarz inequality, and return their term indices.\n> 2. Determine the role of these terms as $A_i$ or $C_i$ based on their coefficients: $A_i$ for positive, $C_i$ for negative.\n>     - (1) If the role is $A_i$, use the first form of the given Cauchy-Schwarz inequality; otherwise, use the second.\n>     - (2) Ensure that the role ($A_i$ or $C_i$) is included among the terms of $S$.\n> 3. Design $B_i$ so that the other role ($A_i$ or $C_i$) is easy to handle.\n> 4. If the Cauchy-Schwarz inequality is applicable, return the corresponding term indices as a list of integers.\n>\n> Provide your analysis and calculation steps, and summarize your answer in a JSON. The JSON format begins with <code>```json</code> as shown below.  \n> Each term should be a LaTeX string without the `$` symbol, and the product sign `*` should be explicitly written between parentheses in the expressions:\n>\n> ```json\n> {\n>   \"applicable\": true or false,\n>   \"role\": \"A_i\" or \"C_i\",\n>   \"term_numbers\": [num1, num2, ...] corresponding to the indices of $A_1/C_1$, $A_2/C_2$, ...\n>   \"B_1\": latex formula corresponding to $A_1$ or $C_1$,\n>   \"B_2\": latex formula corresponding to $A_2$ or $C_2$,\n>   ...\n> }\n> ```\n\nFor each input inequality, we decompose it into individual algebraic terms, assign each term a unique index, and represent them in LaTeX format as a dictionary (`term_dict`).  \nFor example, for the inequality $a^2 + b^2 + c^2 \\geq ab + bc + ca$, the `term_dict` would be  \n`{1: \"a^2\", 2: \"b^2\", 3: \"c^2\", 4: \"-ab\", 5: \"-bc\", 6: \"-ca\"}`.  \nWe also provide the equality condition (`cond_str`) and the assumptions (`assump_str`) as LaTeX strings in the prompt, ensuring the model has access to all relevant information during reasoning.  \nThe prompt instructs the model to analyze the structure of each term to determine its role in the Cauchy-Schwarz inequality as either $A_i$ or $C_i$, and to systematically design the corresponding $B_i$ for each.\n\n#### Post-processing\n\nIn the model response, we extract the relevant terms from `term_dict` according to the `term_numbers` in the JSON, and combine them with the extracted $B_i$ expressions to automatically assemble a standard Cauchy-Schwarz inequality.  \nFor example, if the role is $A_i$, we construct:\n\n$$\n\\left( \\sum_{i} A_i \\right)\\left( \\sum_{i} B_i \\right) \\geq \\left( \\sum_{i} \\sqrt{A_i B_i} \\right)^2.\n$$\n\nAny error encountered during this construction process (as detected by our multiple symbolic checks) is regarded as an exploration failure.\n\n## Method potential\nWe claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its **scalability** in design.  \n\n**Decomposition and search** are our foundational principles, with neuro-symbolic integration and self-improvement as features that can be extended to general inequality proving. This principle is not limited to proving only polynomial or rational function inequalities, but can be generalized to a wide range of inequalities beyond the current scope of Olympiad-style problems. For example, our decomposition approach closely resembles the methodology for solving linear matrix inequalities, supporting the generalization of our framework to this area, potentially with advanced algorithms such as PIETOOLS.  \n\nTo further illustrate this potential, let us consider an example of an integral inequality—an area we are actively investigating as a promising direction for future work.\n\nLet  $f(0) = 0$, $f(x) \\in C^1[0,1] $. Consider the integral inequality\n\n$$\n\\int_0^1 (5 - x^2) f'(x)^2\\,dx \\geq (\\pi^2 + 2) \\int_0^1 f(x)^2\\,dx\n$$\n\nwhich can be established via SOS:\n\n$$\nLHS-RHS=4\\int_0^1 \\left( f'(x) - \\frac{\\pi f(x)}{2\\tan\\frac{\\pi x}{2}} \\right)^2 dx+ \\int_0^1 (1-x^2) \\left( f'(x) - \\frac{f(x)}{x} \\right)^2 dx \\geq 0\n$$\n\nFinally, we wish to avoid making overreaching claims that our method will fundamentally advance general mathematical reasoning or development, as mathematical reasoning itself is both profound and extensive. Nonetheless, we emphasize that **algebraic inequality proving** remains a vast and essential domain, with frequent applications in mathematics and theoretical physics."}, {"review_id": "4lciVhGgfM", "reviewer": "Reviewer_kEQx", "summary": "The paper introduces IneqSearch, a novel hybrid reasoning system designed to automatically prove complex Olympiad-level inequalities. Similar to LIPS system in ICLR'25, this paper combines symbolic computation for rigorous deductive reasoning with large language models (LLMs) for innovative, constructive proof exploration. A key feature of IneqSearch is its iterative learning mechanism, allowing it to continuously expand its theorem database with newly proven results, thereby enhancing its capabilities over time without human intervention. Experimental results demonstrate that IneqSearch significantly outperforms existing methods by successfully solving a high percentage of challenging inequality problems, showcasing the power of integrating symbolic and neural approaches for mathematical reasoning.", "questions": "1.  Formal Proof System Details and Soundness: Please elaborate on the specific formal proof system and verification mechanism used by IneqSearch to \"ensure soundness by constructing verifiable proofs\" and guarantee that \"every theorem in T has been rigorously validated\". How does this internal verification process compare in rigor and automation to the \"automatically verified\" correctness of formal proofs in Lean4 mentioned for baseline solutions?\n    *   Criteria for Score Increase: A clear and detailed explanation of the underlying formal logic or automated verification framework (beyond just human readability of steps) that guarantees the soundness of IneqSearch's proofs would significantly increase the confidence in the system's fundamental \"Quality\" and \"Clarity\".\n\n2.  Computational Budget and Component Performance: What are the typical computational complexity and runtime (latency) characteristics of the Elementary Cyclic Polynomial Decomposition (ECPD) and Sum of Squares (SOS) decomposition algorithms, especially considering SOS is formulated as a semidefinite programming problem? Furthermore, what is the maximum or average time budget allowed per problem for IneqSearch to achieve the state-of-the-art results presented in Table 1? For instance, a comparison point like LIPS specifies a maximum of 1.5 hours per problem.\n    *   Criteria for Score Increase: Providing quantitative details on the computational cost of these core symbolic components and a clear time budget per problem for the reported results would greatly enhance the \"Clarity\" and \"Quality\" of the experimental evaluation, allowing for a more fair and comprehensive comparison of computational resources with other systems.\n\n3.  LLM Error Handling, Backtracking, and Strategy Management: Given that Large Language Models (LLMs) can exhibit \"critical consistency issues\" and \"hallucinations\", how does IneqSearch robustly manage errors introduced by the LLM's \"constructive proof exploration\"? Specifically, what are the mechanisms for backtracking when an LLM-proposed transformation or exploration direction (e.g., \"Inequality Adaption\" or \"Target Shift\" in Figure 2) proves incorrect or unprovable, and how does the system balance or prioritize these various strategies during the iterative trial-and-error process?\n    *   Criteria for Score Increase: A detailed explanation of the system's error recovery, backtracking, and adaptive strategy selection mechanisms would significantly improve the understanding of its \"Quality\" and robustness in handling the inherent unpredictability of LLM-driven exploration, which is crucial for its overall effectiveness as a hybrid system.\n\n4.  Unique Contribution of ECPD to Iterative Learning: Given that Table 2 shows a relatively modest gain (8 problems) from the 'Iterative Learning' component, and external research [1] suggests limitations in LLM-assisted symbolic library learning, could the authors elaborate on the *unique contribution* of ECPD within the iterative learning mechanism? Specifically, does ECPD's role extend beyond initial problem-solving to enhance the *quality* or *reusability* of theorems for subsequent learning, and are there further ablation studies that could demonstrate this?\n    *   Criteria for Score Increase: A clear explanation or additional experimental evidence that elucidates how ECPD, as a symbolic decomposition method, specifically contributes to the robustness, generalizability, or practical utility of the theorems acquired through iterative learning, thereby differentiating IneqSearch's approach from limitations observed in other LLM-assisted symbolic library learning studies, would enhance the understanding of its \"Originality & Significance\" and \"Quality\".\n\n[1] Berlot-Attwell, Ian, Frank Rudzicz, and Xujie Si. \"LLM Library Learning Fails: A LEGO-Prover Case Study.\" arXiv preprint arXiv:2504.03048 (2025).", "limitations": "I generally like this paper, especially on its significant results, the introduction of ECPD, and the surprising effect of iterative learning mechanism. All my concerns are mainly around the clarity of this paper, and I hope this can be addressed in the future version.", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 3, "originality": 2, "strengths_and_weaknesses": "Strengths:\n\n*   Quality & Significance: The paper introduces IneqSearch, a hybrid reasoning system that significantly outperforms existing methods on Olympiad-level inequalities. It successfully proves 342 out of 437 problems and achieves a 100% success rate on the challenging MO-INT-20 dataset. The system's strong performance on high-difficulty problems, which often require multi-step scaling and are non-symmetric or non-homogeneous, highlights its effectiveness where symbolic solvers and LLMs typically fail. An ablation study clearly demonstrates the complementary nature and individual contributions of its components, showing that each added feature boosts performance.\n*   Originality & Significance: IneqSearch's core strength and innovation lies in the ECPD and SOS methods. It reformulates inequality proving as a structured search problem focused on decomposing expressions into non-negative components, a strategy inspired by formal mathematical practice, which further enables effective iterative learning mechanism that autonomously incorporates newly proven results into its theorem database, allowing for continuous knowledge acquisition and enhanced capabilities without human intervention. \n\nWeaknesses:\n\n*   Clarity & Quality (Formal Proof System & Soundness): While the paper states that IneqSearch \"ensures soundness by constructing verifiable proofs\" and that \"every theorem in T has been rigorously validated, guaranteeing the system’s soundness\", the specific details of its formal proof system and verification mechanism are not fully elaborated in the provided excerpts. This leaves ambiguity regarding how its correctness is guaranteed compared to systems like Lean, which have automatically verifiable formal proofs.\n*   Clarity & Quality (Computational Budget & Comparison Fairness): The paper mentions that \"No GPU was used in the experiments\" and \"All computations can be executed on a standard personal computer\". However, key details regarding the computational complexity and exact runtime of the decomposition algorithms like ECPD and SOS are not clearly specified. Without these details, it is difficult to fully assess the fairness of comparisons with other systems, such as LIPS, especially concerning the computational budget required for the main results. The paper also states that the code is not yet ready for publication.\n*   Clarity & Quality (Trial-and-Error Process): The inductive agent proposes \"multiple possible choices at each step\", implying a trial-and-error approach. However, the paper does not explicitly specify the technical details of this trial-and-error process, including any backtracking mechanisms or how the cost associated with failed attempts is factored into the reported computational budget or performance metrics.\n*   Clarity (Theoretical Scope of Decomposition): While the system effectively uses ECPD and SOS for polynomial non-negativity and preprocessing converts fractional expressions to numerator-only forms, the paper does not clearly specify the theoretical completeness of these methods for *all* types of inequalities, particularly in relation to the broader mathematical context of Hilbert's Seventeenth Problem, which deals with *rational functions*. The system primarily operates on polynomials after preprocessing, which may limit its applicability to certain classes of inequalities compared to a universal theoretical claim.\n*   Clarity (Limited Demonstrated Impact and Justification of Iterative Learning's Contribution, particularly ECPD's Role):\nThe paper identifies iterative learning as a distinguishing feature and a key contribution, enhancing IneqSearch's proving capability and scalability by autonomously incorporating solved inequalities into its knowledge base. However, the ablation study in Table 2 shows that the \"Iterative Learning\" mechanism is responsible for solving only an additional 8 problems (from 334 to 342). This comparatively modest gain raises questions regarding the practical significance of this component's overall impact. Furthermore, while Elementary Cyclic Polynomial Decomposition (ECPD) is mentioned as a core method for \"representing and manipulating expressions\" in inequality proofs, its specific and unique contribution to *enhancing iterative learning* (beyond its direct application in the solver) is not clearly demonstrated to be substantial or to significantly overcome limitations that other research (e.g., [1]) might suggest for symbolic library learning. \n\n[1] Berlot-Attwell, Ian, Frank Rudzicz, and Xujie Si. \"LLM Library Learning Fails: A LEGO-Prover Case Study.\" arXiv preprint arXiv:2504.03048 (2025).", "was_revised": true, "final_justification": "Most of my concerns are addressed except for some detailed implementations. Given author's commitment on open source, I would like to raise my score.", "rebuttal": "## 1\nIneqSearch generates **pure algebraic proofs**, whose soundness can be guaranteed and verified by symbolic computation engines. While our proofs are not formally verified by an axiomatic logic system, they are validated through explicit algebraic computation. Our implementation is based on SymPy and Mathematica; below we provide a detailed explanation.\n\nGiven an input expression $F$ to IneqSearch, all possible algebraic manipulations can be divided into three categories:\n\n- **Rewriting**: $F = \\sum_i F_i$, including ECPD transformations, SOS, theorem search, etc.\n- **Inequality Transformation**: $F \\geq 0 \\Leftrightarrow G \\geq 0$, including removing denominators, removing radicals, etc.\n- **Scaling**: $F \\geq G$, used only during LLM exploration.\n\nThe first two types of manipulations are mathematically equivalent.\n\nThe third operation, scaling, is carefully constrained to ensure correctness. For example, when instructing the LLM to apply the Cauchy-Schwarz inequality, $(\\sum A^2)(\\sum B^2) \\geq (\\sum AB)^2$, we directly provide $A$ according to the specific problem and let the LLM construct $B$. Regardless of the choice of $B$, the resulting scaling **always preserves validity**, though it may introduce over-scaling. This procedure is conceptually similar to constructing `tactics` in Lean, as implemented in LIPS.\n\nTo enhance the reliability of our implementation, we employ both symbolic and numerical checks.\n\nFor the final algebraic proof $F \\geq \\sum F_i$, if there is no scaling, _i.e._, the LLM is not involved and $F = \\sum F_i$, we directly verify the equality by symbolic computation. In our approach, each $F_i$ is either a square or a previously established theorem, both of which are non-negative, so the overall proof is guaranteed to be correct. If scaling is involved, we additionally verify that the inequality construction is correct by including assertion statements to ensure symbolic correctness during the construction process.\n\nAdditionally, after removing denominators or radicals, or when scaling occurs, we perform numerical verification by sampling variable values. While not mathematically necessary, this step serves as an extra safeguard against potential implementation errors.\n\n## 2\n**Table 3.** Runtime analysis of the proof workflow on INEQ-437.\n| Module                    | Process                      | Avg. Runtime (s) | Time Budget (s) |\n|---------------------------|------------------------------|------------------|-----------------|\n|                           | ECPD Transform               | 0.6              | 30              |\n|                           | Theorem Search               | 41.6             | 240             |\n|                           | SOS                          | 0.4              | 30              |\n| Solver                    | **Total**                    | **12.3**         | **300**         |\n|                           |                              |                  |                 |\n|                           | Equality Condition           | 17.3             | 180             |\n|                           | Target Shift                 | 19.1             | 180             |\n|                           | AM-GM Ineq. Expl.            | 32.6             | 180             |\n|                           | Cauchy-Schwarz Ineq. Expl.   | 27.3             | 180             |\n|                           | Hölder's Ineq. Expl.         | 41.0             | 180             |\n|                           | Jensen's Ineq. Expl.         | 34.4             | 180             |\n|                           | Tangent Line Ineq. Expl.     | 37.9             | 180             |\n| Inductive Agent (o3-mini) | **Total**                    | **65.8**         | **300**         |\n|                           |                              |                  |                 |\n| **Overall**               |                              | **24.1**         | **900**         |\n\n---\n\n**Table 4.** Comparison of solving time and success rate.\n| Methods                  | Avg. Runtime (s) | Success Rate |\n|--------------------------|------------------|--------------|\n| OpenAI o3-mini           | 63               | 35.2%        |\n| LIPS w/ 120 min budget   | 5187             | 62.5%        |\n| LIPS w/ 90 min budget    | 2946             | 50.3%        |\n| IneqSearch w/o LLM       | 12               | 66.8%        |\n| IneqSearch w/ o3-mini    | 24               | 78.3%        |\n\n\n---\n\nTable 3 summarizes the average runtime and time budget for the main proving steps of IneqSearch with o3-mini on our INEQ-437 benchmark. Only the most time-consuming steps are shown, and steps may not be strictly sequential in practice. Reported runtimes are per single execution, though steps may be called multiple times per proof. For successfully solved problems, IneqSearch requires only 12.3 seconds per problem on average, demonstrating **high efficiency**.\n\nTable 4 shows the average solving time for successful proofs, comparing our method to LIPS and o3-mini. Our approach achieves over a 100× speedup compared to LIPS. However, this direct runtime comparison is not fully fair algorithmically, since most of LIPS's time cost comes from repeated LLM calls.\n\nRegarding computational complexity, IneqSearch relies on several computational tools, and the precise complexity depends on the specific algorithm employed. For theorem search, we utilize `SCIP` for linear programming, and for SOS, we employ `MOSEK` to solve the SDP problem.\n\n## 3\n#### Prompt Template\n\nHere, we present the prompt template used to automate the application of the Cauchy-Schwarz inequality with the LLM.  \n\n> We are solving an inequality problem. Please do not use the code interpreter.  \n>\n> The inequality is:  \n> `{S_str}`\n>\n> We have the following important information:\n>\n> 1. Equality holds for: `{cond_str}`\n> 2. Assumption condition: `{assump_str}`\n>\n> Now, we want to use the Cauchy-Schwarz inequality to scale $S$, so that we can obtain an expression which is easier to handle.  \n> The term indices are:  \n> `{term_dict}`\n>\n> Recall that the Cauchy-Schwarz inequality is:\n>\n> $$\n> \\left(\\sum_{i=1}^n A_i\\right) \\left(\\sum_{i=1}^n B_i\\right) \\geq \\left(\\sum_{i=1}^n C_i\\right)^2\n> $$\n>\n> or\n>\n> $$\n> \\sum_{i=1}^n C_i \\leq \\sqrt{\\left(\\sum_{i=1}^n A_i\\right) \\left(\\sum_{i=1}^n B_i\\right)},\n> $$\n>\n> where $C_i = \\sqrt{A_i B_i}$\n>\n> **Instructions:**\n>\n> 1. Identify the terms that are suitable for the Cauchy-Schwarz inequality, and return their term indices.\n> 2. Determine the role of these terms as $A_i$ or $C_i$ based on their coefficients: $A_i$ for positive, $C_i$ for negative.\n>     - (1) If the role is $A_i$, use the first form of the given Cauchy-Schwarz inequality; otherwise, use the second.\n>     - (2) Ensure that the role ($A_i$ or $C_i$) is included among the terms of $S$.\n> 3. Design $B_i$ so that the other role ($A_i$ or $C_i$) is easy to handle.\n> 4. If the Cauchy-Schwarz inequality is applicable, return the corresponding term indices as a list of integers.\n>\n> Provide your analysis and calculation steps, and summarize your answer in a JSON. The JSON format begins with <code>```json</code> as shown below.  \n> Each term should be a LaTeX string without the `$` symbol, and the product sign `*` should be explicitly written between parentheses in the expressions:\n>\n> ```json\n> {\n>   \"applicable\": true or false,\n>   \"role\": \"A_i\" or \"C_i\",\n>   \"term_numbers\": [num1, num2, ...] corresponding to the indices of $A_1/C_1$, $A_2/C_2$, ...\n>   \"B_1\": latex formula corresponding to $A_1$ or $C_1$,\n>   \"B_2\": latex formula corresponding to $A_2$ or $C_2$,\n>   ...\n> }\n> ```\n\nFor each input inequality, we decompose it into individual algebraic terms, assign each term a unique index, and represent them in LaTeX format as a dictionary (`term_dict`).  \nFor example, for the inequality $a^2 + b^2 + c^2 \\geq ab + bc + ca$, the `term_dict` would be  \n`{1: \"a^2\", 2: \"b^2\", 3: \"c^2\", 4: \"-ab\", 5: \"-bc\", 6: \"-ca\"}`.  \n\n#### Post-processing\n\nIn the model response, we extract the relevant terms from `term_dict` according to the `term_numbers` in the JSON, and combine them with the extracted $B_i$ expressions to automatically assemble a standard Cauchy-Schwarz inequality.  \n\n## 4\nDifferent from library learning as in LEGO-Prover, our self-improvement ability is developed from scratch: we do not require any answer annotations or external supervision. Instead, our system relies on discovering new theorems for difficult cases.\n\nWhen proving an inequality by decomposition, _i.e._, $F = \\sum_i F_i$, the core idea is to find components $F_i$ that can \"support\" $F$. For example, suppose $F = F_1 + F_2$ with $F_1 \\geq 0$ and $F_2 \\geq 0$. It may be that $F \\geq F_1$ holds on the interval $(0,1)$, while $F \\geq F_2$ holds on $(1, +\\infty)$. Only their complementarity allows us to prove $F \\geq 0$ on the entire domain. \n\nAbout self-improvement performance, although the ablation study shows that the self-improvement ability only solved 8 additional problems, this does not imply that its contribution is limited.\n\n(1) Solving 8 more problems is actually a substantial improvement, as these are difficult cases considering that this is the incremental gain after all other methods have been applied. Basic methods can already solve the easy problems, so solving a few more hard problems demonstrates a significant advancement.\n    \n(2) The effectiveness of IneqSearch also depends on the problems in the dataset as illustrated in Section 3.3. With a larger dataset, the benefits of self-improvement would be greater.\n\nECPD is a representation method especially effective for Olympiad-style inequalities. For more general inequalities without symmetric or cyclic structure, however, ECPD offers no particular advantage. This is not a limitation, but rather reflects the framework's flexibility—ECPD is just a convenient and efficient option. IneqSearch does not heavily rely on ECPD."}, {"review_id": "84DIIu5df2", "reviewer": "Reviewer_fNdM", "summary": "The paper introduces IneqSearch, a hybrid reasoning system for automated proofs of multivariate polynomial inequalities common in math Olympiads. The symbolic core first normalizes the problem, then attempts to rewrite the inequality as a sum of elementary cyclic polynomials (ECPD) or a sum of squares (SOS). When this direct route fails, an LLM agent suggests transformations derived from standard lemmas (e.g., Cauchy-Schwarz) that create alternate but equivalent targets. A linear-programming search picks coefficients that express the transformed inequality as a non-negative combination of known theorems. Every successful proof is logged, checked, and appended to the theorem base, letting the system solve progressively harder problems in subsequent rounds.", "questions": "•\tThe solver currently targets multivariate polynomial inequalities in positive variables. What prevents it from handling rational functions, sign-changing variables, or transcendental terms?\n\n•\tHave you identified theoretical or practical obstacles to extending the approach beyond Olympiad-style problems?\n\n\n•\tHow sensitive is performance to the ordering in which new theorems are added?\n\n•\tWhat are the main failure modes of the system (e.g. failure to find decompositions, incorrect inductive transformations), and how might these be mitigated in future work?\n\n•\tHow large is the final theorem database after training, and what are its computational or memory implications for scaling to broader problem sets?\n\n•\tAre there plans to release the code and trained theorem database to enable reproducibility and benchmarking by the community?", "limitations": "•\tEvaluation is restricted to polynomial inequalities with positive variables under Olympiad assumptions; generality to broader mathematical domains is untested.\n\n•\tIterative learning risks compounding errors if incorrect proofs are integrated into the database; the safeguards to prevent this are not fully detailed.\n\n•\tCurrent symbolic solver methods may not generalize to inequalities involving transcendental or higher-order functions.", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\n\n•\tStrong empirical results (however, it needs to be evaluated on more datasets): IneqSearch achieves a 78.3% success rate on INEQ-437 and solves 100% of the MO-INT-20 dataset, outperforming both pure LLM-based systems and prior hybrid methods like AIPS and LIPS.\n\n•\tComprehensive evaluation, including ablation studies demonstrating the contribution of each system component (symbolic solver, inductive agent, iterative learning).\n\n•\tAblation study demonstrating the contribution of each system component (symbolic solver, inductive agent, iterative learning).\n\nWeaknesses:\n\n•\tInconsistent model coverage in Table 1. All three settings (natural-language, Lean 4, and formal verification) should be benchmarked on the same set of LLMs, yet the formal column reports results for only two models, one of which (“4o-mini”) never appears in the natural-language experiment, making direct cross-modal comparisons impossible.\n\n•\tLack of open-weight baselines. The study omits freely available models, hindering reproducibility and preventing the community from validating or extending the findings without paid API access. (also using deterministic sampling or setting a seed)\n\n•\tOrder-dependent accuracy. Reported success rates assume the exact sequence of previously posed questions; performance could drop under a different interaction history, but this sensitivity is neither analyzed nor controlled.\n\n\n•\tMissing comparison with retrieval-augmented generation (RAG). Given that the task involves answering from a fixed corpus, a RAG baseline is essential to demonstrate the advantage of the proposed method over standard retrieval + generation pipelines.\n\n•\tUnavailable code and data. The appendix does not include the implementation or evaluation scripts, so the reported results cannot be reproduced or independently verified.\n\n•\tWhile the iterative learning mechanism is promising, its scalability to larger or more diverse domains is untested; results are currently limited to algebraic inequalities within Olympiad settings.\n\n\n•\tNo analysis of failure modes by problem category (e.g. symmetric vs asymmetric inequalities, degree complexity), which would provide deeper insights for model improvement.\n\n•\tLack of statistical significance testing or variance reporting for experimental results, though the absolute performance gains are substantial.\n\n•\tCrucial implementation details, such as the LP search procedure, SDP solver configurations, and LLM prompting strategies, are missing, making it difficult for readers to reproduce or build upon the work. Additionally, the dataset used is limited.\n\nQuality:\n\nThe paper presents a well-motivated methodology grounded in mathematical practice, with good empirical validation and rigorous decomposition algorithms.\n\nClarity:\n\nThe writing is generally clear and well-organized. Diagrams (e.g. Figures 1–3) effectively illustrate the pipeline and proof construction. \n\nSignificance:\n\nThis work is significant for automated mathematical reasoning, particularly in algebraic inequality proofs, an area of interest for both AI for mathematics and AGI evaluation benchmarks. The hybrid design could inspire extensions to broader formal domains.\n\nOriginality:\n\nThe paper frames inequality proving as a decomposition-based search integrated with LLM-guided inductive exploration, and in its self-improving theorem acquisition paradigm to enrich the database of theorems.", "was_revised": true, "final_justification": "The authors rebuttal addressed some of my concerns partially that led to my increasing my rating for the paper.", "rebuttal": "Thanks for your review.\n\nEven though DeepMind recently used Gemini (with natural language) to win a gold medal in the IMO, our results show that LLMs still face significant limitations in Olympiad inequality proofs. Algebraic inequality proving is exceptionally challenging because it involves navigating an infinite reasoning space and requires both rigorous deductive reasoning and constructive proof techniques. Combining symbolic computation with LLMs enables two complementary modes of thought—rigorous deduction and creative exploration—making this hybrid approach especially powerful for tackling inequalities.\n\n# Takeaways\n\n1. Relying solely on LLMs to generate natural or formal proofs remains challenging. Our work demonstrates that integrating symbolic solvers with LLMs enables hybrid reasoning, resulting in substantial performance improvements. T\n\n2. The decomposition and search framework offers a promising direction for automated inequality proving. By leveraging LLMs for implementation within this framework, our results establish a practical path forward for general automated inequality proving.\n\n# Question response\n## Question 1\nIneqSearch is **Not** limited to multivariate polynomial inequalities (please see dataset.pdf in the supplementary materials). It can also solve inequalities involving radicals, exponents, logarithms, rational functions, and more. These types of inequalities are very common in mathematical Olympiads, so our system faces no fundamental obstacles in handling such problems.\n\nAs illustrated in the paper, cases involving negative variables can generally be addressed with similar methods, although they may require additional case analysis or domain partitioning. If real variables are needed, our system does not encounter any fundamental barriers.\n\n## Question 2\n\nAs we place no restriction on the analytic form of functions, **theoretically** we can solve all inequalities by decomposition, provided that the relevant theorems exist in our theorem database. We also do not assume any initial axioms in the theorem base, any necessary results from other areas can be incorporated as needed, enabling IneqSearch to continually learn and expand its capabilities.\n\nWe conduct experiments on Olympiad inequalities due to the abundance of resources and the relative simplicity of their forms. However, our approach is fully extensible to broader classes of algebraic inequalities. We claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its **scalability** in design.\n\n**Decomposition and search** are our foundational principles, with neuro-symbolic integration and self-improvement as features that can be extended to general inequality proving. This principle is not limited to proving only polynomial or rational function inequalities, but can be generalized to a wide range of inequalities beyond the current scope of Olympiad-style problems. For example, our decomposition approach closely resembles the methodology for solving linear matrix inequalities, supporting the generalization of our framework to this area, potentially with advanced algorithms such as PIETOOLS.\n\nTo further illustrate this potential, let us consider an example of an integral inequality—an area we are actively investigating as a promising direction for future work:\n\nLet  $f(0) = 0$, $f(x) \\in C^1[0,1] $. Consider the integral inequality\n\n$$\n\\int_0^1 (5 - x^2) f'(x)^2\\,dx \\geq (\\pi^2 + 2) \\int_0^1 f(x)^2\\,dx\n$$\n\nwhich can be established via SOS:\n\n$$\n\\text{LHS} - \\text{RHS} = 4\\int_0^1 \\left( f'(x) - \\frac{\\pi f(x)}{2\\tan\\frac{\\pi x}{2}} \\right)^2 dx + \\int_0^1 (1-x^2) \\left( f'(x) - \\frac{f(x)}{x} \\right)^2 dx \\geq 0\n$$\n\n\n\n## Question 3\nThe reported accuracy is **Not** order-dependent. As illustrated in the original paper, we conduct experiments by round (Section 4.4):\n\n> In each round, IneqSearch traverses the entire benchmark and attempts to prove each inequality. The theorem base is updated once after completing the round, ensuring that any newly discovered results become available as tools for subsequent iterations.\n\nThis procedure guarantees that the accuracy does not depend on the order in which inequalities are processed.\n\n## Question 4\n\nWhen a problem fails to be proved, it means IneqSearch has tried all available methods—including finding decompositions and applying various inductive transformations—but none succeeded. Therefore, we are unable to point out a specific stage where the failure occurred; rather, all proof attempts were unsuccessful.\n\nInstead, we can provide an analysis of the error cases, which was somewhat lacking in the original paper. To offer a more intuitive understanding of the difficult cases in the benchmark, we analyze the failed instances to better illustrate the types of challenging problems encountered by IneqSearch.\n\n### Uncommon Equality Conditions\nAs discussed in the Limitation section of the Appendix, a necessary condition for a successful search $F = \\sum_i F_i$ is that all equality cases must be satisfied for each $F_i$. Some problems, however, have uncommon equality conditions. For example,\n\n$$\n\\frac{256}{3125} \\geq x z^4 + x^4 y + y^4 z\n$$\n\nwith $x + y + z = 1$ attains equality when $(x, y, z) = (4/5, 1/5, 0)$ under cyclic permutation. Another illustrative example is\n\n$$\n\\frac{1}{81} \\geq \\frac{xyz}{(x+1)(x+y)(y+z)(z+16)},\n$$\n\nwhere equality holds at $(x, y, z) = (2, 4, 8)$. \n\nSolving such problems often requires more sophisticated, constructive algebraic proofs.\n\n### Non-directly Usable Assumptions\nA significant proportion of problems involve assumptions that are either non-standard or couple the variables in ways that prevent direct normalization or substitution techniques. For example, constraints such as\n\n$$\n\\frac{1}{x+1} + \\frac{1}{y+1} + \\frac{1}{z+1} = 2\n$$\n\nor\n\n$$\nx + y + z + 1 = 4xyz\n$$\n\nmake it challenging for solvers to apply classical inequality lemmas directly.\n\nThe key to addressing such problems often lies in transforming the given condition into a more manageable form, rather than directly substituting it into the inequality.\n\n### Non-homogeneity\nIneqSearch relies on homogeneity information to decompose inequalities. However, the majority of unsolved inequalities in this benchmark are non-homogeneous.\n\nFor example, consider\n\n$$\n8 + 2x^2 + 2y^2 + 2z^2 + xyz \\geq 5x + 5y + 5z,\n$$\n\nwhere the left-hand side contains constant, quadratic, and cubic terms, while the right-hand side is purely linear. The lack of a uniform degree structure complicates both analytic and algorithmic approaches.\n\nSuch non-homogeneous structures often arise from the underlying construction of inequalities involving constants, such as the simple case $x^2 - 2x + 1 \\geq 0$, which contains non-homogeneous terms. The algebraic construction involving constant terms remains a significant obstacle for our symbolic solvers.\n\n## Question 5\n\nAfter learning on our benchmark, we ultimately obtain a total of 171 theorems.  \nIn our implementation, theorem search primarily consists of three steps: formalizing the equation, applying SymPy’s `solve_undetermined_coeffs` function, and solving a linear program using `SCIP`.\n\nThe algorithmic complexity of these components is as follows:\n\n- Equation formalization: This step involves symbolic manipulation and pattern matching, which can be computationally intensive depending on the structure of the input but is typically polynomial in the size of the expression.\n- Solve_undetermined_coeffs: Solving for undetermined coefficients often reduces to solving a system of linear equations, which generally has cubic complexity in the number of variables (i.e., $\\mathcal{O}(n^3)$).\n- Linear programming with SCIP: SCIP solves linear programs in polynomial time for most practical cases, but the worst-case complexity depends on the specific algorithm used and the size of the problem.\n\nIn practice, the main computational bottleneck is the equation formalization step, with a typical runtime between 30 and 40 seconds. If the theorem base becomes very large, we may need to optimize this step further. The memory cost is not significant, as the algorithm filters applicable theorems during equation formalization—typically fewer than 10 theorems.\n\n\n## Question 6\nThe codebase is now ready and will be released upon publication.\n\n# Concerns about LLM comparison\nWe are not very familiar with the specific meaning of the RAG baseline (standard retrieval + generation pipelines) in this context. Our work focuses on inequality proving and general inequality search, with access to a theorem base. Are you suggesting that we should instruct the LLM to retrieve relevant theorems and combine them to construct a proof, similar to how proofs are written in Lean? If so, we are concerned that this approach may not be ideal, as it does not allow for automatic verification or leverage solver-based deduction, and generating proofs directly in natural language may be more natural and straightforward for our setting. We would appreciate it if you could clarify how this task could be naturally formulated as a RAG problem in our case.\n\nFor the open-weight models, we additionally include Qwen3-32B and Llama3.3-70B for natural language proof. On INEQ-437, Qwen3 solves 59 problems and Llama3.3 solves 48 problems, corresponding to solving rates of 13.5% and 10.9%, respectively."}, {"review_id": "SepMywEy1o", "reviewer": "Reviewer_Hdro", "summary": "This paper presents IneqSearch, an inequality prover that utilizes decomposition techniques. Specifically, IneqSearch employs a symbolic solver to identify which theorems are involved in the proof and leverages Large Language Models (LLMs) to instantiate and establish a set of candidate theorems. Additionally, an iterative learning mechanism can be seamlessly integrated into the framework, allowing the theorem library to evolve automatically. Experimental results demonstrate that the proposed method achieves a significant improvement on two Olympiad-level benchmarks.", "questions": "- The authors mention that the natural language solutions generated by LLMs are manually checked by experts. What are the criteria used for evaluating these solutions? \n- The SOS and theorem searcher incorporate numerical optimization methods for semi-definite programming and linear programming. How is the discrepancy between numerical results and symbolic results addressed? For instance, if $λ_i$ is determined to be $1.414$, will it be converted to $\\sqrt{2}$?\n- Figure 1 lacks clarity; it would be beneficial to enhance the illustration of the workflow.\n- More experimental details are needed. For example, what is the average solving time? What prompts were used for generating natural language solutions? Additionally, will the code be made open-source in the end?", "limitations": "Yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths\n- The decomposition-based framework, along with a neuro-symbolic methodology for inequality proving, shows great promise.\n- The framework incorporates an iterative learning strategy, offering an intriguing approach for the self-evolution of the neuro-symbolic system.\n- It demonstrates strong performance on competition-level benchmarks, indicating a promising direction for automatic inequality proving.\n\n### Weaknesses\n- Although the proposed method is extremely effective, it appears to be limited to the domain of inequality proving. It would be beneficial to discuss how this method could inspire advancements in other related fields, such as general mathematical reasoning or mathematical theorem proving.\n- The decomposition-based proving approach, particularly the SOS technique, generates proofs that lack human readability and explicitness. This limitation hinders the method's effectiveness as an educational tool for providing answers and affects its performance when used as training data to enhance models.\n- Evaluating the method on additional benchmarks could further demonstrate its effectiveness. For example, the 567Neq benchmark introduced in LIPS would be a valuable test case.\n- The ablation study indicates that the current iterative learning mechanism has limitations, as it only successfully solves eight additional problems when integrated into the method.", "was_revised": true, "final_justification": "I lean toward borderline acceptance. (1) The proposed symbolic method and experimental results are promising. (2) While I appreciate the self-improvement concept, the current implementation is too limited to justify a higher score.", "rebuttal": "Thanks for your review.\n\nEven though DeepMind recently used Gemini (with natural language) to win a gold medal in the IMO, our results show that LLMs still face significant limitations in Olympiad inequality proofs. Algebraic inequality proving is exceptionally challenging because it involves navigating an infinite reasoning space and requires both rigorous deductive reasoning and constructive proof techniques. Combining symbolic computation with LLMs enables two complementary modes of thought—rigorous deduction and creative exploration—making this hybrid approach especially powerful for tackling inequalities.\n\n# Takeaways\n\n1. Relying solely on LLMs to generate natural or formal proofs remains challenging. Our work demonstrates that integrating symbolic solvers with LLMs enables hybrid reasoning, resulting in substantial performance improvements. T\n\n2. The decomposition and search framework offers a promising direction for automated inequality proving. By leveraging LLMs for implementation within this framework, our results establish a practical path forward for general automated inequality proving.\n\n# Question response\n## Question 1\n\nFor the evaluation, no step credit is given. Only fully correct or incorrect responses are considered. In fact, errors in LLM-generated natural language proofs are often methodological such as employing incorrect logic, reversing the direction of inequalities, or using specific examples in place of general proofs, rather than minor technical mistakes. \n\n## Question 2\nFor linear programming, the variable domain is set to rational. For SDP, numerical values are rationalized using SymPy's `nsimplify` function with a tolerance of 1e-15.  \nIt should be noted that decomposition equalities are checked using symbolic computation to ensure soundness.\n\n## Question 3\n\nPlease specify which parts you find confusing, so that we can improve our paper.\n\n\n## Question 4\n#### Computation time\n**Table 3.** Runtime analysis of the proof workflow on INEQ-437.\n| Module                    | Process                      | Avg. Runtime (s) | Time Budget (s) |\n|---------------------------|------------------------------|------------------|-----------------|\n|                           | ECPD Transform               | 0.6              | 30              |\n|                           | Theorem Search               | 41.6             | 240             |\n|                           | SOS                          | 0.4              | 30              |\n| Solver                    | **Total**                    | **12.3**         | **300**         |\n|                           |                              |                  |                 |\n|                           | Equality Condition           | 17.3             | 180             |\n|                           | Target Shift                 | 19.1             | 180             |\n|                           | AM-GM Ineq. Expl.            | 32.6             | 180             |\n|                           | Cauchy-Schwarz Ineq. Expl.   | 27.3             | 180             |\n|                           | Hölder's Ineq. Expl.         | 41.0             | 180             |\n|                           | Jensen's Ineq. Expl.         | 34.4             | 180             |\n|                           | Tangent Line Ineq. Expl.     | 37.9             | 180             |\n| Inductive Agent (o3-mini) | **Total**                    | **65.8**         | **300**         |\n|                           |                              |                  |                 |\n| **Overall**               |                              | **24.1**         | **900**         |\n\n---\n\n**Table 4.** Comparison of solving time and success rate.\n| Methods                  | Avg. Runtime (s) | Success Rate |\n|--------------------------|------------------|--------------|\n| OpenAI o3-mini           | 63               | 35.2%        |\n| LIPS w/ 120 min budget   | 5187             | 62.5%        |\n| LIPS w/ 90 min budget    | 2946             | 50.3%        |\n| IneqSearch w/o LLM       | 12               | 66.8%        |\n| IneqSearch w/ o3-mini    | 24               | 78.3%        |\n\n\n---\n\nIneqSearch first attempts to prove each inequality using the symbolic solver. If this attempt fails, the system proceeds to call the LLM for further exploration. In our implementation, there are 5 inequality lemmas to be explored, and each inequality exploration calls the LLM once, with one additional retry if the first call is invalid. The exploration of inequality lemmas is conducted in parallel, allowing us to collect all possible valid scaled expressions after exploration.\n\nTable 3 summarizes the average runtime and time budget for the proving steps of IneqSearch with o3-mini on our INEQ-437 benchmark. Only the major time-consuming steps are listed, and the steps are not strictly sequential in the implementation. Other routine algebraic manipulations are omitted, as their runtimes are comparatively negligible. The reported runtime for each process refers to the average time per single execution, although each process may be called multiple times within a proof. For accurate measurement of actual solving time, we report the runtime for successful proofs, where IneqSearch requires only 12.3 seconds on average per problem, demonstrating **high efficiency**.\n\nTable 4 presents the average solving time for successfully solved problems and compares our method to LIPS and o3-mini. Compared to LIPS, our approach achieves more than a 100× speedup in runtime. While these results are convincing in practice, we note that this direct runtime comparison is not entirely fair from an algorithmic perspective, as the majority of the time cost in LIPS arises from repeated LLM calls. Our method is primarily solver-driven and typically requires far fewer LLM calls per problem.\n\nRegarding computational complexity, IneqSearch relies on several computational tools, and the precise complexity depends on the specific algorithm employed. For theorem search, we utilize `SCIP` for linear programming, and for SOS, we employ `MOSEK` to solve the SDP problem.\n\n### Proof template\nFor natural language proof, we directy ask LLM with latex format input, here is one example:\nLet $x,y$ and $z$ be positive real numbers such that $- x - y - z + x y + x z + y z = 0$, prove that $$1 + x + y + z \\geq 4 x y z$$\n\n### Code availability\nThe codebase is now ready and will be released upon publication.\n\n# Concerns\n## Method potential\nWe claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its **scalability** in design.  \n\n**Decomposition and search** are our foundational principles, with neuro-symbolic integration and self-improvement as features that can be extended to general inequality proving. This principle is not limited to proving only polynomial or rational function inequalities, but can be generalized to a wide range of inequalities beyond the current scope of Olympiad-style problems. For example, our decomposition approach closely resembles the methodology for solving linear matrix inequalities, supporting the generalization of our framework to this area, potentially with advanced algorithms such as PIETOOLS.  \n\nTo further illustrate this potential, let us consider an example of an integral inequality—an area we are actively investigating as a promising direction for future work.\n\nLet  $f(0) = 0$, $f(x) \\in C^1[0,1] $. Consider the integral inequality\n\n$$\n\\int_0^1 (5 - x^2) f'(x)^2\\,dx \\geq (\\pi^2 + 2) \\int_0^1 f(x)^2\\,dx\n$$\n\nwhich can be established via SOS:\n\n$$\nLHS-RHS=4\\int_0^1 \\left( f'(x) - \\frac{\\pi f(x)}{2\\tan\\frac{\\pi x}{2}} \\right)^2 dx+ \\int_0^1 (1-x^2) \\left( f'(x) - \\frac{f(x)}{x} \\right)^2 dx \\geq 0\n$$\n\nFinally, we wish to avoid making overreaching claims that our method will fundamentally advance general mathematical reasoning or development, as mathematical reasoning itself is both profound and extensive. Nonetheless, we emphasize that **algebraic inequality proving** remains a vast and essential domain, with frequent applications in mathematics and theoretical physics.\n\n\n## Self-improvement performance\nAbout self-improvement performance, although the ablation study shows that the self-improvement ability only solved 8 additional problems, this does not imply that its contribution is limited.\n\n(1) Solving 8 more problems is actually a substantial improvement, as these are difficult cases considering that this is the incremental gain after all other methods have been applied. Basic methods can already solve the easy problems, so solving a few more hard problems demonstrates a significant advancement.\n    \n(2) The effectiveness of IneqSearch also depends on the problems in the dataset as illustrated in Section 3.3. With a larger dataset, the benefits of self-improvement would be greater."}]

Author rebuttal:

Meta-review: This paper introduces IneqSearch, a neuro-symbolic system for proving Olympiad-level inequalities using structured search. The hybrid approach uses a Large Language Model for guided exploration and a symbolic solver for deductive reasoning, along with an iterative learning mechanism to expand its theorem database over time. On a new benchmark of 437 problems, IneqSearch achieved state-of-the-art performance by solving 78.3% of them, outperforming prior methods.

**(b) Strengths**

*   **Performance:** The system demonstrates impressive, state-of-the-art results on a challenging benchmark of Olympiad-level problems.
*   **Novel Methodology:** The paper presents a sound, hybrid neuro-symbolic framework.
*   **Verifiable Proofs:** Unlike purely generative models, the system produces verifiable algebraic proofs.

**(c) Weaknesses**

*   **Narrow Scope:** The method is highly specialized for Olympiad-style inequalities, and its broader applicability remains unclear.
*   **Initial Lack of Clarity:** The original submission lacked key implementation details, a runtime analysis, and comparisons on standard benchmarks, which initially raised concerns about reproducibility.

The recommendation is to **accept**. The paper makes a significant contribution by achieving outstanding results on a very challenging task. While the initial submission had weaknesses, the authors' comprehensive and diligent responses during the discussion period successfully addressed reviewer's concerns

**(e) Summary of Discussion and Rebuttal**

The discussion period was highly effective. Key points raised by reviewers included the need for evaluation on public benchmarks, clarification on the proof soundness mechanism, and a detailed runtime analysis. The authors addressed these points thoroughly by:

*   Providing new, strong results on the public IneqMath benchmark.
*   Explaining in detail how backend symbolic engines (SymPy/Mathematica) guarantee proof soundness, clarifying that numerical checks are only used as pre-filters.
*   Adding comprehensive analyses of runtime and computational costs.
Decision: Accept (poster)