Thanks for your review.

Even 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.

Takeaways

1. 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

2. 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.

Question response

Question 1

For 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.

Question 2

For 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.
It should be noted that decomposition equalities are checked using symbolic computation to ensure soundness.

Question 3

Please specify which parts you find confusing, so that we can improve our paper.

Question 4

Computation time

Table 3. Runtime analysis of the proof workflow on INEQ-437.

---

Table 4. Comparison of solving time and success rate.

---

IneqSearch 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.

Table 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.

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 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.

Regarding 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.

Proof template

For natural language proof, we directy ask LLM with latex format input, here is one example: Let $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$

Code availability

The codebase is now ready and will be released upon publication.

Concerns

Method potential

We claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its scalability in design.

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.

To 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.

Let $f(0) = 0$, $f(x) \in C^1[0,1]$. Consider the integral inequality

$$\int_0^1 (5 - x^2) f'(x)^2\,dx \geq (\pi^2 + 2) \int_0^1 f(x)^2\,dx$$

which can be established via SOS:

$$LHS-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$$

Finally, 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.

Self-improvement performance

About 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.

(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.

(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.

About Figure 1

For Figure 1, your understanding is correct, we mainly highlight these features to better illustrate our framework. Thank you for pointing out the clarity issue, we will revise the figure to improve its quality.

About theorem generalization

Your point is important and is actually a direction for our future work. Currently, although we can generate a series of theorems from a single problem by adding rules, these theorems are still quite specific in form. Using LLMs to generalize learned theorems is a promising approach and could enable broader application. Our work is actively developing along this direction. We discuss this further in the Discussion section:

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 + bc + cd + da = 1$, show that $\frac{a^3}{b+c+d} + \frac{b^3}{c+d+a} + \frac{c^3}{d+a+b} + \frac{d^3}{a+b+c} \geq \frac{1}{3}$. This problem can be extended to a broader class of inequalities, such as $\sum_{i}^n \frac{x_i^3}{s-x_i} \geq \frac{4k^2}{(n-1)n}$ where $s = \sum_i x_i$ and $k^2=\sum_{i<j} x_ix_j$. The key insight is recognizing that denominators of the form $s - x_i$ and the cyclic condition $ab+bc+cd+da = 1$ can be abstracted to the setting $k^2 = \sum_{i<j} x_ix_j$, 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 to LLMs' strengths.

About code release

We didn't release the code at submission because the project is a bit complex and we hadn't finished organizing it. The codebase is about 1MB of pure Python script. We will make the code open-source to ensure reproducibility.

Thanks for your review.

Even 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.

Takeaways

1. 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

2. 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.

Question response

Question 1

IneqSearch 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.

As 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.

Question 2

As 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.

We 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.

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.

To 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:

Let $f(0) = 0$, $f(x) \in C^1[0,1]$. Consider the integral inequality

$$\int_0^1 (5 - x^2) f'(x)^2\,dx \geq (\pi^2 + 2) \int_0^1 f(x)^2\,dx$$

which can be established via SOS:

$$\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$$

Question 3

The reported accuracy is Not order-dependent. As illustrated in the original paper, we conduct experiments by round (Section 4.4):

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.

This procedure guarantees that the accuracy does not depend on the order in which inequalities are processed.

Question 4

When 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.

Instead, 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.

Uncommon Equality Conditions

As 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,

$$\frac{256}{3125} \geq x z^4 + x^4 y + y^4 z$$

with $x + y + z = 1$ attains equality when $(x, y, z) = (4/5, 1/5, 0)$ under cyclic permutation. Another illustrative example is

$$\frac{1}{81} \geq \frac{xyz}{(x+1)(x+y)(y+z)(z+16)},$$

where equality holds at $(x, y, z) = (2, 4, 8)$.

Solving such problems often requires more sophisticated, constructive algebraic proofs.

Non-directly Usable Assumptions

A 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

$$\frac{1}{x+1} + \frac{1}{y+1} + \frac{1}{z+1} = 2$$

or

$$x + y + z + 1 = 4xyz$$

make it challenging for solvers to apply classical inequality lemmas directly.

The 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.

Non-homogeneity

IneqSearch relies on homogeneity information to decompose inequalities. However, the majority of unsolved inequalities in this benchmark are non-homogeneous.

For example, consider

$$8 + 2x^2 + 2y^2 + 2z^2 + xyz \geq 5x + 5y + 5z,$$

where 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.

Such 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.

Question 5

After learning on our benchmark, we ultimately obtain a total of 171 theorems.
In 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.

The algorithmic complexity of these components is as follows:

• 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.
• 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)$).
• 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.

In 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.

Question 6

The codebase is now ready and will be released upon publication.

Concerns about LLM comparison

We 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.

For 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.

Thank you for your detailed feedback and for engaging with our rebuttal. We would like to address your concluding comment that "many weaknesses are really not addressed." We respectfully believe this stems from a misunderstanding of our work’s core contribution, problem scope, and evaluation standards in automated theorem proving.

Your concerns mainly fall into two categories:

• Evaluation Methodology: Model coverage, missing RAG baseline, lack of statistical metrics.
• Contribution Scope: Scalability and absence of some failure analyses.

Our main argument is that these are not unaddressed weaknesses, but rather reflect a misalignment between standard empirical ML evaluation frameworks and our task, which is deterministic, search-based, and logic-driven.

We focus specifically on Olympiad-level inequality proving—a recognized grand challenge where past methods have struggled. The value of our work lies in its depth and success in this difficult subdomain.

Below, we clarify our choices and their alignment with standards in our field:

---

• Model Coverage

Table 1 benchmarks IneqSearch against SOTA methods within their respective categories, not for direct cross-modal comparison.

Fair SOTA Comparison: In the formal proof setting, LIPS [1] is the main SOTA baseline. For fairness, we used the same language model as LIPS to evaluate IneqSearch.

Uniqueness: IneqSearch uniquely generates pure algebraic proofs verifiable by symbolic computation. No other method produces this output, so direct comparison in this aspect was not possible.

• RAG Baseline

A RAG baseline is not appropriate for our core mechanism. As LeanDojo [2] and others show, RAG excels at premise selection, while IneqSearch is a symbolic solver performing deterministic, algebraic decomposition—a structured search, not a retrieval task. Formulating it as RAG would not yield a meaningful baseline.

• Statistical Metrics

These metrics do not apply to our evaluation context. Theorem proving is deterministic: for any problem, a proof is either found or not. This binary evaluation is standard in ATP. As in recent work on inequalities [1,3], geometry [7], and general ATP [2,4,5,6], statistical metrics are not reported due to the deterministic nature of the task.

• Scalability

We have demonstrated in the rebuttal how our framework generalizes within inequality proving, including to integral inequalities, illustrating its scalability.

• Error analysis

To address this limitation, we provide a supplementary error analysis broken down by problem category. Specifically, Table 5 presents the results for symmetric versus non-symmetric inequalities, as well as for polynomial and non-polynomial problems:

Table 5. Analysis of key properties

---

Table 6. Analysis of polynomial inequalities by degree

We hope these clarifications comprehensively address the remaining concerns. We are confident that IneqSearch represents a substantial and well-validated contribution to automated mathematical reasoning and kindly ask for a reconsideration of our work.

Reference

[1] Wei, C., Sun, M., & Wang, W. (2024). Proving olympiad algebraic inequalities without human demonstrations. NeurIPS 37, 82811-82822.

[2] Yang, K. et al. (2023). LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. NeurIPS Datasets and Benchmarks.

[3] Li, Z. et al. (2025). Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning. ICLR 2025.

[4] Ren, Z. Z. et al. (2025). Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv:2504.21801.

[5] Lin, Y. et al. (2025). Goedel-prover: A frontier model for open-source automated theorem proving. arXiv:2502.07640.

[6] Li, Z. et al. (2024). A Survey on Deep Learning for Theorem Proving. 1st Conf. on Language Modeling.

[7] Trinh, T. H. et al. (2024). Solving olympiad geometry without human demonstrations. Nature, 625, 476-482.

Thank you again for your valuable time and positive re-evaluation. We are very encouraged by your willingness to raise our score and truly appreciate that our explanations have been effective.

Our ultimate goal is to ensure our work is not just acceptable, but a clear and strong contribution that you can support with confidence. We feel we are on the cusp of addressing all major concerns, thanks in large part to your insightful guidance.

To help us cross that final hurdle, we would be immensely grateful if you could share what you see as the most significant remaining reservation or the key aspect that currently prevents you from fully recommending acceptance.

Understanding this final piece of the puzzle would be incredibly valuable to us. We are committed to resolving any remaining issues and hopefully earning your enthusiastic support for our paper.

Thank you once more for your constructive and open dialogue.

1

IneqSearch 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.

Given an input expression $F$ to IneqSearch, all possible algebraic manipulations can be divided into three categories:

• Rewriting: $F = \sum_i F_i$, including ECPD transformations, SOS, theorem search, etc.
• Inequality Transformation: $F \geq 0 \Leftrightarrow G \geq 0$, including removing denominators, removing radicals, etc.
• Scaling: $F \geq G$, used only during LLM exploration.

The first two types of manipulations are mathematically equivalent.

The 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.

To enhance the reliability of our implementation, we employ both symbolic and numerical checks.

For 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.

Additionally, 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.

2

Table 3. Runtime analysis of the proof workflow on INEQ-437.

---

Table 4. Comparison of solving time and success rate.

---

Table 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.

Table 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.

Regarding 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.

3

Prompt Template

Here, we present the prompt template used to automate the application of the Cauchy-Schwarz inequality with the LLM.

We are solving an inequality problem. Please do not use the code interpreter.

The inequality is:
{S_str}

We have the following important information:

1. Equality holds for: {cond_str}
2. Assumption condition: {assump_str}

Now, we want to use the Cauchy-Schwarz inequality to scale $S$, so that we can obtain an expression which is easier to handle.
The term indices are:
{term_dict}

Recall that the Cauchy-Schwarz inequality is:

$$\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$$

or

$$\sum_{i=1}^n C_i \leq \sqrt{\left(\sum_{i=1}^n A_i\right) \left(\sum_{i=1}^n B_i\right)},$$

where $C_i = \sqrt{A_i B_i}$

Instructions:

1. Identify the terms that are suitable for the Cauchy-Schwarz inequality, and return their term indices.
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.
   • (1) If the role is $A_i$, use the first form of the given Cauchy-Schwarz inequality; otherwise, use the second.
   • (2) Ensure that the role ($A_i$ or $C_i$) is included among the terms of $S$.
3. Design $B_i$ so that the other role ($A_i$ or $C_i$) is easy to handle.
4. If the Cauchy-Schwarz inequality is applicable, return the corresponding term indices as a list of integers.

Provide your analysis and calculation steps, and summarize your answer in a JSON. The JSON format begins with <code>```json</code> as shown below.
Each term should be a LaTeX string without the $ symbol, and the product sign * should be explicitly written between parentheses in the expressions:

{
  "applicable": true or false,
  "role": "A_i" or "C_i",
  "term_numbers": [num1, num2, ...] corresponding to the indices of $A_1/C_1$, $A_2/C_2$, ...
  "B_1": latex formula corresponding to $A_1$ or $C_1$,
  "B_2": latex formula corresponding to $A_2$ or $C_2$,
  ...
}

For 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).
For example, for the inequality $a^2 + b^2 + c^2 \geq ab + bc + ca$, the term_dict would be
{1: "a^2", 2: "b^2", 3: "c^2", 4: "-ab", 5: "-bc", 6: "-ca"}.

Post-processing

In 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.

4

Different 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.

When 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.

About 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.

(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.

(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.

ECPD 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.

Thank you for the detailed rebuttal. I now have a better understanding of the technical details behind the system. However, I still find several critical issues unresolved. Therefore, I will maintain my current score, leaning toward a negative recommendation. Below are my follow-up comments and questions:

1. On the Underlying Verification Mechanism

While I agree that expressing the target expression as a sum of squares (SOS) is sufficient to guarantee non-negativity, I believe some important details in the verification process remain unclear:

(1) Algebraic transformations without scaling

You mention that in the absence of scaling, the correctness of transformations can be verified symbolically. Given the wide variety of possible transformations (e.g., removing radicals, substitutions, removing denominators), can all such manipulations be soundly verified using symbolic computation? If so, could the authors specify which tools (SymPy, Mathematica, etc.) and what exact implementations or algebra systems are used?

(2) Assertions under scaling

You note that when scaling is involved, correctness is ensured via assertion statements. Could you clarify what these assertions entail? For instance, in Figure 3, if a scaling is introduced under certain assumptions, how are these assumptions checked and validated in the backend system?

(3) Use of numerical sampling

You mention numerical sampling as an extra check. However, this is not a valid substitute for formal proof, and could introduce a major unfair advantage for your system. For comparison, the LIPS system uses cylindrical algebraic decomposition (CAD) as a numerical guide, but ultimately still requires formal proof checking in Lean. If IneqSearch treats numerical checks as proof, this would significantly inflate your system’s apparent accuracy compared to fully verified baselines.

2. On Runtime and Search Dynamics

In Table 3, several elementary inequalities (e.g., AM-GM, Cauchy-Schwarz) are reported to take ~30 seconds with o3-mini, while the average total runtime per problem is ~24 seconds. This suggests minimal backtracking or retries during LLM exploration.

• Does this imply that o3-mini is already capable of selecting and executing the correct scaling strategies in one pass?

• If so, how do you reconcile this result with prior work (e.g., Sheng et al. [1]) which found that o3's unreliable performance in inequality reasoning?

3. On the Prompt Template and Absence of Backtracking

Thank you for providing the Cauchy-Schwarz prompt template. However, I do not see any mechanisms related to backtracking or retrying failed strategies. Does this mean your system currently does not implement backtracking?

While you do mention issues like over-scaling, it is unclear whether your system can recover from such situations via LLM-guided search.

4. On Self-Improvement and Decomposition Strategy

I appreciate the authors’ clarification on how decomposition contributes to solving harder problems. I agree that solving 8 additional cases in difficult settings is a meaningful improvement. However, I have a few questions regarding search efficiency:

• How is the search space structured and traversed when attempting to discover helpful decompositions?

• Specifically, how is ECPD (Extended Cyclic Polynomial Decomposition) combined with theorem search or decomposition to improve search efficiency in complex cases?

Overall, I acknowledge the strengths of the system and the improvements over prior work. However, I remain concerned about the rigor of proof validation, the lack of backtracking, and the potential inflation of success rates via numerical heuristics. I hope the authors can address these points in future revisions.

[1] Sheng, Jiayi, et al. "Solving Inequality Proofs with Large Language Models." arXiv preprint arXiv:2506.07927 (2025).

Thank you for your detailed follow-up and for providing us the opportunity to clarify these key technical aspects of our system. We appreciate your insightful questions, which help us articulate the finer points of our methodology. We address each of your concerns below.

On the Underlying Verification Mechanism

We agree that the rigor of the verification process is paramount. Our system's soundness is guaranteed by backend symbolic engines.

(1) All non-scaling manipulations are handled by SymPy and Mathematica. Key operations are implemented and verified as follows:

• Substitutions & Simplification:
  The ECPD transform is implemented in Mathematica by solving the system $C_{k_1, k_2, \ldots, k_m}^{(n)} = \sum_{cyc} x_1^{k_1} x_2^{k_2} \cdots x_m^{k_m}$.

  (* symPolyEqs defines the relation between original and ECPD bases, vars are x_i *)
  sol = Solve[symPolyEqs, vars, Reals]
  varsVals = vars /. sol[[1]]
  F_ECPD = Simplify[F>=0]
  

• Removing Denominators:
  For a fractional expression $F = P/Q$, we use SymPy to separate numerator and denominator, then prove the sign of $Q$ before simplifying.

  P, Q = sympy.together(F).as_numer_denom()
  

• Removing Radicals:
  We use SymPy's unrad to eliminate radicals where possible, then check the co-factors (cov_unrad) to ensure validity.

  F_unrad, cov_unrad = sympy.solvers.solvers.unrad(F)
  

• Final End-to-End Verification:
  A proof is successful if and only if the final equality $F = \sum_i F_i$ holds symbolically, where each $F_i$ is non-negative.

  is_correct = sympy.simplify(F - sum(Fi)) == 0
  

  This ensures the composite proof step is correct, even if individual manipulations are not formally checked.

(2)
The "assertions" we perform are concrete symbolic checks to ensure a proposed scaling is constructed and applied correctly. For example, in Figure 3, where $F = (1 + \frac{1}{x})(1 + \frac{1}{y})(1 + \frac{1}{z}) - 64$, with $x + y + z = 1$:

• After expanding $F$, we provide the LLM with a dictionary of terms {1: 1/x, 2: 1/y, 3: 1/(x*y), ...}.
• The LLM proposes a construction (e.g., Cauchy-Schwarz application) via JSON; we assert the JSON is well-formed and that each B_i is a valid LaTeX formula.
• The system constructs and verifies the scaling inequality programmatically. For the example: $$\left(\frac{1}{x} + \frac{1}{y} + \frac{1}{z} + \frac{1}{xy} + \dots\right) \left(x + y + z + xy + \dots\right) \geq (1+1+1+1+1+1+1)^2$$ The resulting inequality is then passed to the solver. For other lemmas (e.g., Jensen's), we assert/verify convexity as needed.

(3)
Numerical sampling is NEVER used as a substitute for proof. It only acts as a fast heuristic filter to discard obviously false LLM suggestions or catch bugs.

On Runtime and Search Dynamics

Your observation about average runtime is correct. The overall average (24s) is lower than the Inductive Agent's (66s) because many problems are solved directly by our symbolic solver without LLM involvement. The 65.8s runtime reflects the harder problems that require LLM exploration.

Regarding o3-mini's performance, our findings are consistent with IneqMath[1]. LLMs like o3 have "fragile deductive chains," and our system is specifically designed to mitigate this:

• Role Separation: The LLM is a heuristic strategist only; rigorous deduction and verification are offloaded to the symbolic engine.
• Performance Consistency: The differing o3-mini success rates (35.2% vs. 9.5%) are explained by dataset differences. Our benchmark is broader; IneqMath is focused on very hard Olympiad problems.

On the Prompt Template and Absence of Backtracking

Our prompt does not include backtracking logic. This is intentional, as backtracking is managed by the main solver's search algorithm, not the LLM agent.

• Retry: One retry is allowed for superficial LLM failures.
• Backtracking: Handled by our solver's best-first search; if a scaling leads to a dead-end, other nodes are explored. This is systematic and LLM-agnostic.

On Self-Improvement and Decomposition Strategy

Thank you for acknowledging the significance of solving 8 additional hard problems. The search for a decomposition $F = \sum \lambda_i f_i$ is formulated as an LP problem, solving for coefficients $\lambda_i \geq 0$. The search space of $f_i$ is all the theorem base.

ECPD significantly improves the search for symmetric/cyclic problems by providing a canonical basis, dramatically pruning the search space. For example, in Figure 3, $xy + yz + zx - 63xyz + 2$ has 4 variable terms in its original form but only 2 in ECPD ($C_{1,1}^{(3)}$ and $C_{1,1,1}^{(3)}$). This reduction allows more effective theorem filtering and a much smaller, tractable LP problem.

We hope these explanations resolve your concerns. We are confident in the rigor of our symbolic verification and the design of our system.

# Parse and validate the LLM's proposal
try:
    t1 = parse_latex(rsp_dict['t1'])
    ft1 = parse_latex(rsp_dict['f(t1)'])
    assert applicable and ineq.has(ft1)
except:
    return None

# Generate and verify the "proof obligation" for convexity
t = sp.Symbol('t', real=True, positive=True)
coeff = ineq.coeff(ft1)
ft1c = coeff*ft1
ft2 = ft1c.subs({t1:t})
diff1 = sp.diff(ft2, t)
diff2 = sp.diff(diff1, t)
is_convex = sp.solve_univariate_inequality(diff2>=0, v)

# Construct new inequality
if is_convex:
    all_perms = cyclic_permutations(ineq.free_symbols)
    avg_term = 0
    for perm in all_perms:
        j_t = ft1.subs(perm, simultaneous=True)
        coeff = ineq.coeff(j_t)
        j_v = t1.subs(perm, simultaneous=True)
        avg_term += j_v*coeff
    
    ineq_new += n*ft1.subs({t1:t}).subs({t:avg_term/n})
    ineq_new -= ft_sum
    return ineq_new

# Determine validity
c_point = cond_equation[t1]
c_dict = {t:c_point}
ft3 = ft2.subs(c_dict) + diff1.subs(c_dict)*(t-c_point)
is_valid = sp.solve_univariate_inequality((ft2 - ft3)>=0, v)

# Construct new inequality
if is_valid:
    ineq_new = ineq
    ft3c = ft3.subs({t:t1})
    ineq_new -= ft1_sum
    ineq_new += sum_cycle(ft3c)

Now, we address your specific questions, starting with the role of our solver.

On Scaling Strategy Generation and Solver Verification

What exact type of solver is used here?

This is a crucial point that strikes at the heart of our contribution. The "solver" to which a new inequality is passed is not a separate, third-party tool. It is IneqSearch itself.

The process is recursive. When a scaling strategy is applied, it transforms the problem into a new, often simpler, inequality. This new inequality is not handed off to a different component; instead, it is pushed back onto the main best-first search stack as a new sub-goal to be solved by the entire IneqSearch framework.

Therefore, the LLM agent $\mathcal{M}$ is best understood as a powerful heuristic function that the main search algorithm $\mathcal{S}$ can call upon when it needs to expand its search space with a creative, strategic move.

How do you ensure the solver execution strictly follows the assumptions?

This is handled naturally by the recursive architecture described above. When $\mathcal{S}$ validates a lemma (e.g., Jensen's), it generates new proof obligations (e.g., "prove $f''(x) \geq 0$"). These obligations become new sub-goals in the search tree, which must be solved by the same IneqSearch engine. The main proof branch is only allowed to proceed if all of its dependent obligations are successfully discharged.

How does the LLM identify scaling strategies on complex expressions?

We acknowledge that our current design has a specific focus. Our philosophy is to find an overall decomposition of the problem. While this may miss some highly localized tricks, we believe it is a robust approach for a general-purpose solver. This is a deliberate design choice that favors global structure over micro-level manipulation.

On Runtime and Pattern Matching Efficiency

Your analysis of the low number of scaling steps is correct, and it points to a deliberate design choice. As shown in Figure 1, the solving pipeline is a sequence of $\mathcal{S} \rightarrow \mathcal{M} \rightarrow \mathcal{S} \rightarrow \mathcal{M}\rightarrow \dots$. We set the maximum number of exploration calls to $\mathcal{M}$ to 2. This is because IneqSearch is designed to rely on its self-improvement mechanism (learning new theorems for $\mathcal{S}$) to tackle complexity, rather than performing "heavy exploration" (deep, multi-step scaling searches) within a single proof attempt.

On Backtracking and Dataset Implications

Is the backtracking time included in the latency numbers reported in Table 3?

Yes. To be precise: the runtimes for specific processes (e.g., "Equality Condition") are the average times per single, successful execution. The "Total" and "Overall" runtimes are for the entire proof process. Therefore, backtracking time is included in the "Total/Overall" numbers, as it is part of the work done by the main best-first search algorithm in $\mathcal{S}$.

Could you also report runtime statistics on a dataset such as MO-INT-20?

This is an excellent suggestion. To test our system's performance on harder instances, we have run our system on the MO-INT-20 dataset. We report the detailed, per-problem solving times for MO-INT-20 in Table 5 of our revised manuscript. These results provide a clear picture of our system's performance on more difficult problems.

Table 5. Runtime (in seconds) for each problem in MO-INT-20.

We hope this detailed architectural clarification and the new results fully address your concerns. Thank you again for your thorough engagement.

Thanks for your review.

Even 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.

Takeaways

1. 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

2. 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.

Question response

Question 1

IneqSearch 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.

Given an input expression $F$ to IneqSearch, all possible algebraic manipulations can be divided into three categories:

• Rewriting: $F = \sum_i F_i$, including ECPD transformations, SOS, theorem search, etc.
• Inequality Transformation: $F \geq 0 \Leftrightarrow G \geq 0$, including removing denominators, removing radicals, etc.
• Scaling: $F \geq G$, used only during LLM exploration.

The first two types of manipulations are mathematically equivalent.

The 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.

To enhance the reliability of our implementation, we employ both symbolic and numerical checks.

For 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.

Additionally, 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.

Question 2

For 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. Similarly, we performed three independent runs of LIPS and considered a problem solved if at least one run succeeded.

Concerns

Inductive Agent Configuration

Prompt Template

Here, we present the prompt template used to automate the application of the Cauchy-Schwarz inequality with the LLM.
Other exploration prompts are similar and will be included in the revised version.

Prompt for Cauchy-Schwarz Inequality Exploration

We are solving an inequality problem. Please do not use the code interpreter.

The inequality is:
{S_str}

We have the following important information:

1. Equality holds for: {cond_str}
2. Assumption condition: {assump_str}

Now, we want to use the Cauchy-Schwarz inequality to scale $S$, so that we can obtain an expression which is easier to handle.
The term indices are:
{term_dict}

Recall that the Cauchy-Schwarz inequality is:

$$\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$$

or

$$\sum_{i=1}^n C_i \leq \sqrt{\left(\sum_{i=1}^n A_i\right) \left(\sum_{i=1}^n B_i\right)},$$

where $C_i = \sqrt{A_i B_i}$

Instructions:

1. Identify the terms that are suitable for the Cauchy-Schwarz inequality, and return their term indices.
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.
   • (1) If the role is $A_i$, use the first form of the given Cauchy-Schwarz inequality; otherwise, use the second.
   • (2) Ensure that the role ($A_i$ or $C_i$) is included among the terms of $S$.
3. Design $B_i$ so that the other role ($A_i$ or $C_i$) is easy to handle.
4. If the Cauchy-Schwarz inequality is applicable, return the corresponding term indices as a list of integers.

Provide your analysis and calculation steps, and summarize your answer in a JSON. The JSON format begins with <code>```json</code> as shown below.
Each term should be a LaTeX string without the $ symbol, and the product sign * should be explicitly written between parentheses in the expressions:

{
  "applicable": true or false,
  "role": "A_i" or "C_i",
  "term_numbers": [num1, num2, ...] corresponding to the indices of $A_1/C_1$, $A_2/C_2$, ...
  "B_1": latex formula corresponding to $A_1$ or $C_1$,
  "B_2": latex formula corresponding to $A_2$ or $C_2$,
  ...
}

For 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).
For example, for the inequality $a^2 + b^2 + c^2 \geq ab + bc + ca$, the term_dict would be
{1: "a^2", 2: "b^2", 3: "c^2", 4: "-ab", 5: "-bc", 6: "-ca"}.
We 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.
The 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.

Post-processing

In 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.
For example, if the role is $A_i$, we construct:

$$\left( \sum_{i} A_i \right)\left( \sum_{i} B_i \right) \geq \left( \sum_{i} \sqrt{A_i B_i} \right)^2.$$

Any error encountered during this construction process (as detected by our multiple symbolic checks) is regarded as an exploration failure.

Method potential

We claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its scalability in design.

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.

To 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.

Let $f(0) = 0$, $f(x) \in C^1[0,1]$. Consider the integral inequality

$$\int_0^1 (5 - x^2) f'(x)^2\,dx \geq (\pi^2 + 2) \int_0^1 f(x)^2\,dx$$

which can be established via SOS:

$$LHS-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$$

Finally, 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.

Thanks for your review.

Even 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.

Takeaways

1. 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

2. 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.

Question response

Question 1

IneqMath 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%.

Question 2

Table 3. Runtime analysis of the proof workflow on INEQ-437.

---

Table 4. Comparison of solving time and success rate.

---

IneqSearch 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.

Table 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.

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 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.

Question 3

Since 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.

Uncommon Equality Conditions

As 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,

$$\frac{256}{3125} \geq x z^4 + x^4 y + y^4 z$$

with $x + y + z = 1$ attains equality when $(x, y, z) = (4/5, 1/5, 0)$ under cyclic permutation. Another illustrative example is

$$\frac{1}{81} \geq \frac{xyz}{(x+1)(x+y)(y+z)(z+16)},$$

where equality holds at $(x, y, z) = (2, 4, 8)$.

Solving such problems often requires more sophisticated, constructive algebraic proofs.

Non-directly Usable Assumptions

A 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

$$\frac{1}{x+1} + \frac{1}{y+1} + \frac{1}{z+1} = 2$$

or

$$x + y + z + 1 = 4xyz$$

make it challenging for solvers to apply classical inequality lemmas directly.

The 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.

Non-homogeneity

IneqSearch relies on homogeneity information to decompose inequalities. However, the majority of unsolved inequalities in this benchmark are non-homogeneous.

For example, consider

$$8 + 2x^2 + 2y^2 + 2z^2 + xyz \geq 5x + 5y + 5z,$$

where 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.

Such 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.

Concern about limited domain

We claim that our method holds significant potential for automated algebraic inequality proving, primarily due to its scalability in design.

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.
To 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.

Let $f(0) = 0$, $f(x) \in C^1[0,1]$. Consider the integral inequality

$$\int_0^1 (5 - x^2) f'(x)^2\,dx \geq (\pi^2 + 2) \int_0^1 f(x)^2\,dx$$

which can be established via SOS:

$$LHS-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$$

Finally, 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.