Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Authors: Zenan Li
Zhaoyu Li
Wen Tang
Xian Zhang
Yuan Yao
Xujie Si
Fan Yang
Kaiyu Yang
Xiaoxing Ma
Venue: ICLR 2025 Poster (2025)
Keywords: Neuro-symbolic theorem proving
Olympiad inequalities
Large language model
Symbolic method
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We introduce LIPS, a powerful prover for Olympiad-level inequalities.

Abstract: Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the available training data for formal proofs is limited, posing a significant challenge to LLM-based tactic generation. To address this, we introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods. The key aspect of this integration is identifying which parts of mathematical reasoning are best suited to LLMs and which to symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure~1). We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions, achieving state-of-the-art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.

Published as a conference paper at ICLR 2025
PROVING OLYMPIAD INEQUALITIES BY SYNERGIZING LLMs AND SYMBOLIC REASONING
Zenan Li Zhaoyu Li:; Wen Tang', Xian Zhang', Yuan Yao', Xujie Si,, Fan Yang",
Kaiyu Yang"! Xiaoxing Ma
State Key Lab of Novel Software Technology, Nanjing University, China, 2 University of Toronto," 3 Peking University, Microsoft Research, 5 Meta FAIR
1llz2smaaii .aaiiinjjuu www.nnuu........ edu, en, zhaoyu@cs toronto. edu zhxian@microsoft com, kaiyuy@meta com, xxmên ju. edu.cm
Problem
Chen
2014]:
If a, b, c positive reals and a² b²
c² 1, then
1
+ 1
+
S 6ab + c² +
(1)
a
+
2 62
+2 2
c² +
6bc + a
6ca + 6
Figure 1: We prove inequality problems math Olympiads that involve a finite number of real vari- ables, hypotheses, and one conclusion. Both the hypotheses and the conclusion consist of constants, variables, algebraic operations (e.g., addition, multiplication), and transcendental functions like exp.
ABSTRACT
Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (a.k.a. tactics) within proof system. However, the space possible tacties is vast and complex, while the available training data for formal proofs is limited, posing significant challenge to LLM-based tactic generation. To address this, we introduce neuro-symbolic tactic generator that synergizes the mathematical intuition learned by L.LMs with domain-specifie insights encoded by symbolic methods. The key aspect of this integration is identifying which parts mathematical reasoning are best suited to LLMs and which symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure ! We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics com- petitions, achieving state-of-the-an art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.
INTRODUCTION
Automated theorem proving has been a long-standing goal in Al (Newell & Simon 1956). Recent research explores leveraging large language models (LLMs) generate formal proofs that can be verified in formal proof systems like Lean (de Moura et al. 2015), opening a new avenue to theo- rem proving (Li al. 2024 Yang al.] 2024). This promising approach has already led to tools that assist human mathematicians (Song et al.) 2024) and the first AI that achieves silver-medal performance in the International Mathematical Olympiad (IMO) (Google Mend 2024).
While based proof generation shows great promise across various mathematical domains, its performance is constrained by the scarcity of formal proof data. Furthermore, it remains an open
"Equal contribution. This work was partially done during Zenan's 's internship at MSRA. I Equal advising. All experiments were conducted outside Meta's compute infrastructure.

---

Published as a conference paper at ICLR 2025
Current inequality problem
New inequality problem
Inequality sequence (Proof)
G, c. three reals, prove that
Given b, b three reals, prove that
Given u,b, three reals, prove that ab bc oz & +b*
+ a' +
V(ze +00)22
3. scate Souchy_Schaare Buars
Tactic generation & pruning
Goal filtering & ranking
((sa² 6PX(2e + 6P) o²
K + 83) + 6-) of c.
② View' + 6')(2e 6.) s +
2. scale AM GM 2vors
ab + be 3
(a bo)
2 b² + 2c" 4.
$ d' +c²
Symtooli--feeedd scoling
1.. ranking
2 iiplify
abb 1) + +-blc ()) c c) 3ab 3he + Rea (a of
ot + 62+ set
QEDI
LLM generated rewriting
Symbooli flleerigg
An overview of our neuro-symbolic inequality prover LIPS. By integrating both LLMs and symbolic methods in an iterative process of tactic generation and goal selection, can generate human-readable and formally verifiable proofs in Lean for Olympiad-level inequality problems.
Figure 2:
problem whether LLMs can perform precise and complex symbolic manipulations (Hammond & Leake 2023). To address these limitations, mechanical symbolic reasoning is still essential. Un- like L.L.Ms symbolic methods leverage domain- -speciii knowledge to achieve greater efficiency and generalization without relying extensive training data (Wu) 2008; Heule et al. (2166). Integrating LLMs with symbolic methods presents a promising strategy for tactic generation and theorem prov- ing. This raises a key question: Which aspects of mathematical reasoning are best suited to LLMs, and which to symbolic methods? By exploring this question, we aim to combine the strengths of both approaches effectively. Since symbolic methods are inherently domainn-spcciff concrete domain: inequalities, which offers a balance between feasibility and practicality.
focus
Mathematical Inequalities. Incqualities arise from various branches of mathematics (Hardy al. 1952]. Their proofs often rely on a relatively small set of fundamental techniques, yet these tech- niques can be applied in remarkably intricate and nuanced ways. In this paper, further constrain our scope to elementary algebraic inequalities (Figure[]). which were prevalent in high-school math- ematics competitions (Manfrino et al. 2010)) e.g., Problem 2 in IMO 2000. Additionally, these inequalities are closely related to quantifier-fre free real arithmetic in satisfiability modulo thcories (SMT) (Barrett & Tinelli (2018), which have numerous practical applications formal verification.
Even this restricted class of inequalities poses significant challenges that surpass the capabilities of current symbolic or neural provers. Symbolic methods (Yang) 1999 Uray 2020) partition the vari- able space (e.g.. R33 for three variables) into a finite number of cells, which are then exhaustively enumerated. These approaches suffer from combinatorial explosion and quickly become compu- tationally infeasible for competition-leve problems. Furthermore, due to their enumerative nature, these methods are black boxes that cannot produce human-readable proofs. On the other hand, neural approaches (Wu et al.) 2 Wei al. 2024) fine-tune language models to generate formal proofs by predicting tactics or evaluating subgoals during proof search. However, due to data scarcity and difficulties in generalization, they frequently underperform certain types of problems.
Our Approach. We introduce LIPS -ased inequality prover with symbolic reasoning), neuro-symbolic framework that synergistically combines LLMs with domain-specinf symbolic techniques, as illustrated in Figure 2 Specifically, we analyze common proving strategies used by humans in inequality proofs and categorize them into two types of tactics: scaling and rewriting. Scaling tactics apply existing lemmas (e.g., the Cauchy-Schward the current goal. The set of lemmas finite, and each lemma can be applied only in a limited number of ways. Therefore, we can enumerate all possible scaling tactics using symbolic tools. However, not all scaling tacties are useful for the current goal; over-scaling may render the goal invalid. We filter out such invalid scaling by using symbolic tools such as SMT solvers to check for counterexamples of the resulting goals. Rewriting tactics, on the other hand, transform a term into an equivalent form (e.g., subtracting 2ab from both sides of the current goal). Any term can be rewritten in infinite ways, making exhaustive enumeration impossible. To address this, we use LLMs to generate rewriting tactics by designing series of prompts for different rewriting formats. By leveraging the mathematical intuition embedded in LLMs, we implicitly prune the infinite tactic space, sampling the most promising equivalent transformations.
inequality) to scale a subterm in
2

---

Published as a conference paper at ICLR 2025
Scaling and rewriting the current goal leads to set of subgoals with new inequalities to prove. Efficient proof search requires prioritizing the most promising subgoals for further exploration. To this end, we employ two strategies: symbolic filtering and neural ranking. In symbolic filtering, use heuristics based on inequalities' homogeneity and decoupling properties to filter out unpromis- ing subgoals. In neural ranking, the remaining subgoals are fed into an LLM,, which compares and ranks them using thahhuht- prompting (Wei et al. 2022). After filtering and ranking, we end up with small number of ranked subgoals. We then iteratively generate and apply new tactics, filter and rank the resulting subgoals, until the final goal becomes trivially provable, resulting in proof that is both human -eanable and formally verified by Lean.
We evaluate LIPS on 161 challenging inequalities collected from three problem sets (Chen 2014
Tung, 2012 Wei et al. 2024). The experimental results show that LIPS consistently achieves state- of-the-art performance and significantly outperforms existing neural and symbolic methods in both effectiveness and speed. Remarkably, out of 61 inequality problems soureed from various math Olympiad competitions, LIPS successfully proves 56 within 90 minutes, whereas the previous best approach proves only 41 problems and fails to generate human-readable proofs.
2 INEQUALITY THEOREM PROVING
In this section, we briefly review existing neural and symbolic methods for inequality proving. In nutshell, symbolic methods complete proofs by exploring the problem space exhaustively, whereas neural methods use LLMs to sample proof steps from a vast tactic space. Each approach comes with distinct advantages and challenges.
2.1 SYMBOLIC METHODS
Consider a set of polynomial inequalities $ DO 0,j = I,.... : m. where DIE (5,22,2,,,)) and each polynomial is defined over n variables as + (2 Fn Li=1 22 x
cylindrical algebraic decomposition (CAD) (Arnon et al., 1984 Caviness Johnson 2012 Kre-
mer 2020) divides the variable space Ih' into multiple connected semi-algebraic sets, known as
cells. Within each cell, the sign of every polynomial remains constant (positive, negative, or zero).
Figure 6(a) illustrates this process with an example of CAD-produehts
cells for two intersecting unit circles. By exploiting this sign invariance, we can determine the satisfiability of inequalitics by enumerating and checking all the cells, rather than searching the entire infinite space IR..
CAD and its variants have been extensively utilized in modern SMT solvers (Jovanovć & de Moura 2013 Kremer et al. 2022: Uncu et al. 2023)_ For inequality theorem proving, CAD transforms the problem into an enumeration task, exhaustively examining all cells to assess whether the inequality can be satisfied. While it is capable, CAD's performance remains unsatisfactory for several reasons. Firstly, CAD's heuristic strategies are primarily designed to efficiently find counterexamples rather than to optimize the proof search process. Secondly, CAD's proving mechanism fails to generate explicit and interpretable reasoming paths, hindering both automatic verification by existing interac- tive theorem provers and human interpretation of the proofs. Additionally, CAD suffers from double exponential computational complexity relative to the number of variables n (Davenport & Heintz, 1988], causing its efficiency to decrease significantly as the number of variables increases. Specifi cally, when dealing with nonlinear inequalities involving fractions radical expressions, auxiliary variables are always introduced to eliminate these terms (e.g., converting /01+ + /äz + a = into
(x4 + 2y + = 0, x² = 11, 2² = T2 > 0, 23 > 0}). Although this transformation successfully rewrites the inequality into polynomial form, it drastically degrades the performance of CAD.
2.2 NEURAL METHODS
In contrast to symbolic methods based on CAD, some approaches leverage neural networks to pre- dict tactics within an interactive theorem prover, generating human-like, step-by-step formal proofs. Specifically, these inequality proofs are typically structured in top-down sequential manner, where each tactic either transforms the current goal into a new subgoal or directly completes the proof (see Figure 6(b)). Figure ((c))pppp provides example proof of the inequality ab + be + ca S a² + 62 + +c.
Among existing work, INT (Wu et al., (02T)) designs a theorem generator for elementary-level in- equalities by randomly sampling axioms from fixed set. It trains Transformer (Vaswani al.,
3

---

Published as a conference paper at ICLR 2025
2017) model to predict tactics and utilizes another value network with the Monte Carlo tree search to complete proofs. Similarly, AIPS (Wei et al., (024) implements a synthetic generator that can produce IMO-level inequalities and trains language model to score each inequality expression in curriculum manner, performing a best-first search to solve these problems. However, their inequal- ity generators have some restrictions either limited in difficulty
constrained by specific forms like cyclic symmetry. Moreover, these approaches mainly rely on fine-tuning models on large-scale datasets, making them highly dependent on the quantity and diversity of the training data.
3 TACTIC GENERATION AND PRUNING
Compared to general theorem proving, the tactics used in inequality proofs are more well-structured: Common tactics can be categorized into two types, namely scaling and rewriting (Lee) 2004 lke-
naga 2018). Scaling refines the given inequality using a known inequality lemma, such as the arithmetic and geometric means (AM-GM) inequality, while rewriting transforms given inequality into an equivalent form, such as multiplying both sides by two. Scaling and rewriting have distinct characteristics. The number of lemmas that can be used in scaling is finite, whereas the number of equivalent transformations in rewriting can be infinite, which leads to different strategies for tactic generation. Furthermore, unlike rewriting, scaling does not preserve the provability of the inequality, leading to different strategies for pruning the resulting subgoals.
Let's consider the inequality problem in Figure edge, the proof for this problem is not readily available online, and neither the most advanced LLMs (e.g., OpenAI 03-mini and DeepSeek- RI) nor existing CAD solvers can solve this inequality.
running example. To the best of our knowl-
3.1 SCALING TACTICS
Given an inequality lemma (e.g., the special case of the AM-GM inequality u² + x2 > 2wv), we enumerate all possible ways to instantiate its arguments (u and v) so that it matches a part of the current proof goal. This is classical problem called e-matching (De Moura & Bjørner [007]] Moskal et al. (2088) and can be solved using existing symbolic tools (Willsey et al. 2021). However, introduces challenge due to the potentially large number of possible patterns. In our running example, there are a total of 162 possible pattern matches for the two-variable AM-GM inequality,
including cases like {u := == v2), {u := i, Va=42
Since scaling tacties refine the inequality goal, they may produce potentially incorrect subgoals (i.e.. unprovable statements). For instance, applying the AM-GM inequality with the pattern {u := a, u = v2} would transform the original incquality into
I
6ab + c² +
+
(2)
2a
2/2b
2/2c
6bc + a²
6ca + b²
However, this inequality does not hold when = b = c= x Specifically, out of the 162 possible patterns for applying the AM-GM inequality in our running example, only six (i.e., {u := a, == 6} and its symmetric cyclical versions) yield correct deductions. Therefore, we propose using CAD to identify counterexamples in the new inequality goals and eliminate the scaling tacties that produce them. Moreover, since most scaling tactics are incorrect and thus induce counterexamples, CAD can efficiently detect and discard them using well-established heuristic strategies.
To further enhance the efficacy and efficiency of scaling tactic pruning, we propose several additional methods to complement CAD in searching for counterexamples:
Quick Check via Test Cases. When CAD identifies a counterexample for scaling tactic, store it as a "test case". For any subsequent scaling tactic, we will perform a quick check using this test case before invoking CAD to determine if the counterexample invalidates the tactic.
Incorporating Numerical Optimization. Since most inequality problems are differentiable, we also use gradient-base based optimization
effective alternative when CAD fails. Specifically,
rewrite the inequality f(æ) < g(x) into min, ig(x) f(x)], and then integrate Newton's 's method
with simulated annealing to solve it (Fu & Su 2016: Ma et al. 2019
Ni et al. 2023).
4

---

Published as a conference paper at ICLR 2025
Utilization of Prior Knowledge. Additionally, prior knowledge be leveraged in scaling tactic pruning when the specific form of am inequality problem is known. For example, the inequalities generated and evaluated by AIPS (Wei et al. 2024) cyclically symmetric and sufficiently tight to achieve equality. Consequently, AIPS verifies the consistency of equality conditions across multiple tacties and discards subgoals that either violate these conditions or do not conform to the desired form. However, to accommodate a broader range of inequalities, our current framework does not incorporate such priors, even though this information could efficiently prune scaling tacties.
3.2 REWRITING TACTICS
After pruning, only few scaling tactics are applicable. For example, we may choose apply the two-variable AM-GM inequality (with pattern {u := a, v == bj and its cyclical versions) and derive a new proof goal from the initial goal (T), formulated as
<
a +
+ 2
+2
30 302
302 36 + a²
3a²
362 + 82
To solve the current proof goal, we need some equivalent transformations. For example, one may simplify the proof goal by replacing 36"436"+2" with 3-2c² using the assumption a² 1 + + 1. However, figuring out effective ways to transform the goal needs creativity and cannot be readily automated through brute-force methods. Consequently, relying solely on symbolic pattern matching tends to be highly ineffective. Moreover, the argument space for rewriting tactics is typically infinite. For example, the assumption a² 6² + o² inequality, significantly enlarging the space of possible rewriting tactics.
can be inserted almost any point within the
To generate and prune the rewriting tactics, we propose directly prompting an LLM to generate candidates. Specifically, for different types of rewriting (c.g., rearrangement, simplification, denom- inator cancellation, etc.), we design tailored prompts that guide the L.MM transform the current proof goal into an appropriate form. The details of these prompts can be found in Appendix C In this setting, tactic pruning is performed implicitly leveraging the algebraic intuition of LLMs, thereby effectively reducing the space of possible rewriting tactics.
Besides neural-guided rewriting, we incorporate two additional symbolic rewriting tactics: the sum- of-squares (Chen) 2013) and the tangent line (Li) 2005) tricks. The sum-of-squares trick attempts to transform the current expression into a summation of non- neg-tnettivv terms, c.g., proving 2x + 2xy - 3z + y² + 2 2 by recognizing 2x + 2zy 3r + y² + 4 (z + y)² + (x ))² The tangent line trick is a powerful variable substitution technique that is frequently used to tackle inequality problems in math competitions.
GOAL. FILTERING AND SELECTION
Scaling and rewriting tactics yield a collection new proof goals. By combining these newly generated goals with existing unexplored ones, we can derive candidate set. The next step is to select the most promising goal from this candidate set for subsequent proving. our running example, we can derive 16 new proof goals from the current goal (3). Below, present three of these new goals, each derived by applying the twovbbri AM-GGM inequality, the three-variable Titu inequality, and simplifying using the given assumption a² 82 2² 1, respectively:
<
2
(4)
G2
2
122
+
+2
a2
+ 312
362
12
3a + 36
② + 3a² + 312
1
9
+ @
(5)
a²
2
12
2
42
7a
712
+
7
1
1
(6)
2
42
02 + 2
2a
20
2c
To select proof goals effectively, existing methods often train language model as value function to evaluate and rank each goal in the candidate set. However, limitations in data quantity and diversity can significantly degrade the performance of these fine-tuned models. For example, the largest.
5

---

Published as a conference paper at ICLR 2025
collected inequality dataset in Lean comprises only 46K samples (Ying et al. 2024), while the largest synthesized dataset of competition-leve inequalities contains merely 191K cyclically symmetric instances (Wei et al. 2024). Consequently,
opt to directly employ off-the-shelf LLM (e.g., GPT-4o) without fine-tuning. However, as more proof goals accumulate, the context length required for prompting LLM for goal ranking becomes substantial, potentially leading the issue of LLMs being "lost in the middle" (Liu et al. (202)). To address this, we propose dividing the goal selection pipeline into two stages: symbolic filtering and neural ranking.
4.1 SYMBOLIC FILTERING
First, we eliminate proof goals that are less promising based carefully designed symbolic rules. Specifically, we prioritize two key properties: (1) homogeneity, meaning both sides of the inequality have the same degree (c.g., a² + b > 2ab); and (2) decoupling. which refers to whether the inequal- ity contains mixed-variable terms (e.g.. abc considered coupled). Both properties are reasonable criteria for prioritization. Regarding homogeneity, most substitution and transformation tactics pre- serve homogeneity. Hence, homogeneous inequality allows for a broader range of tactics to be applied, thereby producing more valuable proof goals. For decoupling, inequality with fewer coupled terms is not only clearer but also amenable to greater variety of techniques, such as the cum-of-square and tangent line tricks.
To measure decoupling and homogeneity, we first approximate the proof goal by polynomial in- equality using Taylor expansion. We then compute the expectation of the number of variables in each term and the variance of the degree of each term, respectively. Formally, given a polynomial
inequality expressed as ((x1,... .......... 2n.) and homogeneity score (HM) are computed as:
E 0g 2f1 r O, the decoupling score (DC)
h I111 > 0)), HM(
k Σ j=1
DC(
Σ 1=1
04
Σ
(d:
dz)
1 1=1 K:
where d; i1 +... in is the total degree of i-th term in the inequality.
worth noting that the homogeneity score and the decoupling score are not always consistent. In our running example, the newly generated goals in 4 (5). and (6) achieve homogeneity scores of 0.56, 0.55, and 0.80, and decoupling scores of 0.44, 0.48, and 0.66, respectively. As a result, we normalize the scores into [0, and then compute the average score to filter the candidates.
4.2 NEURAL RANKING
Symbolic rules are not universally effective, Hence, we use these rules solely to eliminate unpromis- ing proof goals, leaving top-k candidates, for final selection by an LLM. Unlike symbolic filtering, which requires explicit definitions of inequality metrics, we use the chain-of th--uuhhttthhhtt prompting (Wei) al.) 2022, Chu et al., (203) query an LLM rank the proof goals based on their proving difñ- culty. The detailed prompt for the running example is shown below.
Prompt of neural ranking
am trying to prove the original inequality: If a, b, e are positive reals and a² + 6² e² 1, then
I 30"400=p02 + 3nd 36 3n 3ar43 and transform it into the following
x-42 1442
incqualities.
(1)
2442 S 22 2
a2436" aet
243a2
(2)
< 7a
(3)
2242
2242 S 3-2a2 3-262
3-2.2
Your task is to rank the transformation results in descent order. Note that
Please reason step by step;
More meaningful transformation, i.e., reduce the proving difficulty. should ranked higher:
3. Put the index of selected inequality within (bxxed(()) egg., \......e..........e..... ((Dxxe((())2))3))

---

Published as a conference paper at ICLR 2025
Table 1: Proof success rates (%) on three datasets. LIPS consistently outperforms baselines.
Neural Provers
Symbolic Provers
Dataset # of Problems
LIPS
DSP
MCTS
AIpst
CAD²
MMA#
ChenNEQ
41
0.0
17.0
70.7
68.2
95.1
24.4
MO-INT
20
0.0
15.0
50.0
60.0
60.0
80.0
20,01
567NEQ
100
0.0
4.0
54.0
52.0
68.0
14.0
Total
161
0.0
8.6
59.0
57.1
76.3
17.31
We include the results reported by the AIPS paper since the code is not publicly available. CAD and MMA only output verification results, they cannot produce human-readable proofs.
EXPERIMENTS
In this section, conduct a series of experiments address the following three research questions:
RQ1: Efficacy Can LIPS prove more problems compared to existing methods?
RQ2: Efficiency- -
-Can LIPS obtain proof' in less time compared to existing methods?
RQ3: Scalability - Can LIPS be improved by using more scaling lemmas or more powerful LLMs?
5.1 EXPERIMENTAL. SETUP
Datasets. We evaluate LIPS on three datasets: ChenNEQ. MO-INT-20, and 567NEQ, respectively. ChenNEQ consists of 41 Olympiad-leve inequalities collected by Chen 2014); MO-INT is new competition-lewe inequality benchmark introduced in AIPS (Wei et al. 2024). featuring 20 prob- lems sourced from IMO shortlists and various national mathematical Olympiads; 567NEQ consists of 567 hard inequalities created by Tung (2012) and we randomly selected 100 problems from the original problem set the testbed for our framework. To formalize the problems in Lean 4, directly translate the LaTeX source code into Lean using manually defined rules.
Baselines. We compare LIPS with five baselines: DSP (Jiang et al. 2023b), CAD (Kremer 2020 MMA (Wolfram Research), MCTS (Wu et al. (02T), and AIPS (Wei et al. 20224.. DSP consists of two steps, natural language reasoning generation and proof autoformalization, and we instantiate the LLM used in each step GPT-4o. MCTS (Monte Carlo tree search) has been explored in previ- ous studies (Wu et al. 202T) and serves as an alternative method for proof goal selection. ATPS an inequality prover system based on SymPy, which has demonstrated the capability to prove competition-lewe inequalities. CAD integrates series of CAD-based inequality solvers including Z3 (De Moura & Bjørner 2008), CVC5 (Kremer et al., 2022), RC-CAD (Lemaire et al. (2005), and Bottema (Lu 1998). MMA, referring to Mathematica, incorporates the CAD algorithm with other reduction strategies, providing a powerful algebraic system for inequality verification (Wolfram Re- search 2020). Further implementation details for the baseline methods are provided in Appendix C
Implementation. The detailed processes of tactic generation, goal selection, as well as the overall framework are provided Appendix B To construct the tactics, we design total of 96 scaling tactics and 16 rewriting tactics, each formalized in Lean 4. The corresponding premises and LIM prompts are summarized in Appendix(C For the counterexample search in scaling tactic pruning, we integrate four CAD-based solvers (Z3, CVC5, RC-CAD, and Bottema) and implement optimizer based on SciPy (Virtanen et al. 2020). For the LLM involved in transformation tactic generation and proof goal ranking, the filtered goal set to 10, as it is the largest size that ensures GPT-4o's s efficacy. The code, together with the experimental data, is available at httptttt////t https:://gitubb com zn- zn w NeqIIIP
GPT-40 (version Azure-0501). In symbolic filtering,
fix the size of
5.2 EXPERIMENTS
RQ1: Efficacy. We evaluate the proof success rates of LIPS and the five comparative methods across the three datasets. For each proving task, a time limit of 90 minutes is imposed, consistent with that of AIPS and the standard problem-solving time constraint in the IMO. The overall results are presented Table [ First, we observe that the neural methods (DsP and MCTS) cannot achieve satisfactory performance. An analysis of DsP's results reveals that GPT-4o is unable to provide ac-
7

---

Published as a conference paper at ICLR 2025
100
36
pruning rallo (%6)
AIPS JJPS
Number of itteratoon
30-
24.
$0
18-
70
14 15 16
4
10 11
13
15 16 17
Indox of successfully proved problems
Iodox of successtally proved problems
Figure 3: Tactic pruning ratio (f. higher better) and number of iterations (L). The results illustrate that the tactic pruning method of LIPS is very stable, and outperforms the existing method by 7.92% on average. Furthermore, the high efficiency of LIPS is derived from accurate goal selection, allow- ing proof to be successfully constructed with a small number of goal selection iterations.
curate natural language solutions or generate precise formal proofs in the Lean 4 language, resulting a zero success rate. Alternatively, MCTS struggles to effectively identify the correct reasoning path among numerous proof goals, causing many proving attempts to terminate due to timeouts. We also evaluate the performance of the recent OpenAl ol op-evvwwww model on the MO-INT dataset. Through manual inspection of the generated natural language answers, find that none of the problems are correctly solved. Examples of these neural methods are provided in Appendix [E]
Symbolic provers outperform neural provers, CAD and MMA achieve overall success rates of 59.0% and 57.1%, 1, respectively. However, LIPS further surpasses symbolic provers by a significant margin of 14.0% 24.4%. Notably, symbolic provers fail to produce any human- reeaanereadable reasoning path. In contrast, the proofs generated by LIPS are not only accessible and human-readable, but also have been successfully verified by the Lean theorem prover. For reference, include two examples (one showcasing a successful proof and the other demonstrating a failed attempt) in Appendix
RQ2: : Efficiency. Since existing methods are built on different deduction engines, direct compar- ison of their proving time could be unfair. Instead, we break down the efficiency evaluation into two aspects, i.e., the pruning ratio of scaling tactics and the number of iterations in goal selection. Given that AIPS uses the equality check as the scaling tactic pruning strategy, we compare this approach with the CAD-based strategy employed in LIPS. Figure providde the result of each problem in the MO-INT dataset. LIPS outperforms the existing method in 13 out of 20 problems, and achieves an average improvement 7.92%.
Furthermore, we count the number of goal selection iterations for each successfully proved problem, and present the results in Figure 3 Due to the absence of a comparison method, we only include the oracle (i.e., optimal goal selection) as a reference. We can observe that LIPS performs no more than 33 search loops to successfully obtain a proof, and for 12 out of 16 problems, it exceeds the oracle by fewer than 10 steps. In addition, LIPS requires an average of 15.75 search loops, which is only 2.17 times that of the oracle (7.25), demonstrating that LIPS's 's efficiency also stems from its high accuracy in generating proving paths.
RQ3: Scability. We conduct four experiments on the ChenNEQ dataset to explore the scalability of LIPS's symbolic and neural components. For the symbolic part, we first examine how expanding the scaling tactics affects the performance of LIPS. To this end, we randomly select 7 sets of scaling tactics with varying sizes and plot the performance curve in Figure 4(a). The results show that the proof success rate consistently increases as more scaling tactics are included, suggesting potential benefits in further enlarging our scaling tactic library. The second experiment investigates the effect of different sizes of the filtered set. The corresponding performance curve is shown in Figure (bb) We observe that the success rate remains robust (over 85%) with sizes from 8 to 16, but decreases significantly when the set is either too small or too large.
For the neural part, we explore the performance LIPS with different LLMs serving in rewriting tactic generation and neural ranking. We select three alternative LLMs. i.e., Mathstral 7B (Jing et al. 2023a), LLaMA-3 8B (Al 2024). and DeepSeek-chte V2.5 (DeepSeek-A] 2024). We also in- clude baseline method s simplife liff function instead of existing LLM-based rewriting tactics. In neural ranking, we directly random selection as the baseline. The proving success rates are provided in Figure 5 The
ablative study. In rewriting tactic generation, the baseline uses SymPy
8

---

Published as a conference paper at ICLR 2025
300
[00
Proving success rote (%)
100
80-
Proving sucecas
60
Proving sucpess
75
312
12
124
50
Various sizes scaling tactios
Various sizes
Taetic Cienerstion
Neuni Ranking
Various LLMSs in rowriling tactic generation and neural ranking
Figure 4: Performance curves across different scaling Figure 5: Performance of various LLMs as tactics and filtered set sizes, Results indicate that: (1) alternatives. Results illustrate that: (1) LLMs Adding scaling tactics consistently improves the prov- are crucial in rewriting tactic generation and ing success rate; (2) The effectiveness of symbolic fil- neural ranking; (2) The more powerful LLM tering and the size the filtered set are critical factors. can achieve higher proving success rate.
sults demonstrate that all three alternative LLMs exhibit strong mathematical intuition, achieving performance comparable to GPT-4o in neural ranking. However, there exists a small decline in per- formance for rewriting tactic generation, which may be due to differences in instruction following and mathematical reasoning capabilities.
A blation study. To showease the strength of our neuro-symbolic paradigm, we present the results of removing neural or symbolic modules of LIPS in Appendix D We also analyze the performance of symbolic solvers, offering guidance on optimal time limit settings in LIPS.
Case study. Besides the rumning example (T) we provide two additional examples in Appendix F illustrate that LIPS can discover new proofs. which are previously unavailable online. Moreover, we also present two examples in Appendix [F) to demonstrate that users can verify human-written proofs by comparing them with the reasoning paths generated by LIPS.
RELATED WORK
Symbolic Tools for Mathematical Reasoning. Symbolic tools are essential for performing ex- act computations and formal reasoning in mathematics. Interactive theorem provers such as Is- abelle (Paulson 1994). Cog (Cog) 1996). and Lean (de Moura et al., 2015) enable users build verifiable proofs manually, ensuring correctness through rigorous formal logic. These systems have been instrumental in formalizing and verifying significant mathematical theorems, including the Four Color Theorem (Gonthier] 2008) and the Kepler Conjecture (Hales et al.] 2017). Alternatively, some symbolic reasoning tools aim solve mathematical problems without human intervention. Automated theorem provers like E (Schulz) 2002) and Vampire (Kovács & Voronkov 2013) are designed to prove mathematical statements by systematically exploring possible proofs within a logical framework, particularly excelling in first-order logic. SMT solvers such Z3 (De Moura & Bjomner 2008) and CVC5 (Barbosa et al.) (202)) determine the satisfiability of logical formulas with respect background theories like arithmetic, bit-vectors, and arrays by integrating logical reason- ing with theory-speciff decision procedures. Computer algebra systems like Mathematica (Wolfram) Research). Maple (Heck & Koepf [193), and SymPy (Meurer et al. 2017) manipulate mathemat- ical expressions symbolically, supporting functionalities such as simplification, differentiation, in- tegration, and equation solving. Despite their capabilities, these automated solvers struggle with competitive mathematical problems and often cannot generate human readable reasoning steps.
Machine Learning for Formal Theorem Proving. There a longstanding tradition of leveraging machine learning techniques to automate theorem proving (Urban et al. 2008 Gauthier et al.) 2017
Zhang et af., 2021 Piotrowski et al. 2023 Bllauwbrook et al., (202)). Recently, the emergence of LLMMs has expanded the potential of these techniques, offering new opportunities for automating
theorem proving (Li et al. 2024 Yang et al. 2024). A line of research (Polu Sutskever 2020
Wu et al. 1021 Han et al. 2022 First et al. 2023 Yang et al. 2023: Xin et al.) 2024a Lin et al.
2025) fine- tunes pre-trained language models on large-scale scale formal datasets to predict the tactics
given a proof goal. Alternative approaches (Jiang et al. 2023b Xin et al. 2024b Zhao et al. 2024
Zheng et al., 2024; Thakur et al.) (024) integrate LLMs into structured prompt frameworks for formal theorem proving, leveraging information such as natural language proofs feedback from

---

Published as a conference paper at ICLR 2025
Lample et al. [022] Polu et al. 2023| Wang et al. [003] Wei al. 2024) also train LLMs as value networks to evaluate each subgoal and guide the proof search to completion. However, these methods primarily rely on LLMs to prune the search space, and their performance heavily depends on the quality and diversity of the training data, which may limit their generalizability notable exception and closely related work to ours is AlphaGeometry (Trinh et al.] (024), which uses language model only to predict auxiliary construction rules, after which its symbolic solver automatically enumerates all inference rules to generate the proof in a specialized language used in GEX (Chou et al., 2000). Compared their approach, our neuro-symbolic framework generates step-by-step proof's in general-purpose formal language Lean and allows for integrating arbitrary symbolic tools that do not require direct proof generation. Furthermore, our focus on inequality problems spans a much wider range of complex mathematical skills than plane geometry problems. Our techniques could serve as a solid foundation for broader areas of mathematical research such as information theory (Dembo et al. [991). optimization (Nesterov) 2013), and deep learning (Roberts) et al. 2022). making it a suitable pathway to more advanced mathematical problems.
interactive theorem provers. Some methods (Polu & Sutskever 2020:
novel or more complex mathematical problems. A
7 LIMITATIONS AND FUTURE WORK
While LIPS has shown significant promise in generating formal proofs for Olympiad inequalities, several avenues remain open for enhancement and expansion.
Automating the Formalization of Tactics. Our framework currently relies on a set of manually crafted tactics for scaling and rewriting inequalities, such various forms of AM-GM inequality. This manual effort may impact scalability, given that the effectiveness of our approach is closely tied to the breadth of available tacties. Future work could focus on automating the discovery, formaliza- tion, and proof of new tactics to expand the tactic library. Developing methods for automatic tactic generation would reduce human effort and enhance the framework's 's scalability and adaptability.
Enhancing the Reasoning Capabilities of LLMs. We leverage the mathematical insights learned by LLMs in our framework, and there is potential further improve their reasoning performance. One promising direction is to collect or generate additional formal inequality problems and their corresponding proofs to create a richer dataset for fine-tuning I.LMs specifically for this task. Some existing techniques (Li et al. 2025) may be useful for generating diverse and high-quality problems to enhance the LLMs' capabilities in handling inequalities, leading to better overall performance.
Broadening the Application Domain. While our framework currently focuses on Olympiad-level elementary algebraic inequalities, extending to more complex problems, such as concentration inequalities in machine learning theory, presents an exciting avenue for future research. This would involve improving the symbolic solver to handle inequality structures that consist of infinite vari- ables and higher-order concepts like expectations or variances. Developing efficient algorithms and symbolic reasoning methods for these advanced mathematical constructs could significantly broaden the applicability of our neuro-symbolic paradigm. Extending our approach to other mathematical domains holds great potential and is promising direction for future work.
8 CONCLUSION
In this paper, we introduce a neuro-symbolic framework for generating formal proof' that integrates the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods, specifically focusing on the domain of Olympiad inequalities. We categorize the tactics used in inequality proofs into two types: scaling and rewriting. Symbolic methods are employed to generate and filter scaling tactics by applying set of lemmas through mechanical symbolic reasoning. LLMs are leveraged to generate rewriting tacties, implicitly pruning the infinite num- ber of equivalent transformations to a manageable set. We further combine symbolic tools with LLMs to prune and rank subgoals, enhancing the efficiency of proof search. Experiments on chal- lenging inequalities from three problem sets show that our neuro-symbolic inequality prover LIPS significantly outperforms both LLMs and symbolic methods, demonstrating the effectiveness of the neuro-symin symoolyc integration and laying solid foundation for its adoption in broader domains.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGMENT
We appreciate anonymous reviewers for their valuable comments and engaging discussions. This work was partially conducted during Zeman's 's and Wen's internships at MSRA. it supported by the National Natural Science Foundation of China (Grants #62025202) and the Frontier Technologies R&D Program of Jiangsu (BF2024059). Zhaoyu Li and Xujie Si were also supported, in part, by In- dividual Discovery Grants from the Natural Sciences and Engineering Research Council of Canada, and the Canada CIFAR AI Chair Program. Xian Zhang (zhxi an @mi crosoft. com), Kaiyu Yang (kai yuyyytee com), and Xiaoxing Ma (xxmên n juu. edu. cn) are the corresponding authors.
REFERENCES
Meta AI. Llama 3 model card. 2024. URL htt.:/ttt//ggthhhee www/met.- lama / ama bblo/mmain/M0EE CARD md
Dennis Aronn, George E Collins, and Scott McCallum. Cylindrical algebraic decomposition The basic algorithm. SIAM Journal on Computing, 1984.
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Ab- dairhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cve5: A versatile and caauustral-strengtee SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2022.
Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. 2018.
Lasse Blaauwbrock, Mirek Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2Tac: Online representation learning of formal math concepts. In International Conference Machine Learning (ICML), 2024.
Bob Caviness and Jeremy R Johnson. Quantifier elimination and cylindrical algebraic decompo- sition. Springer Science & Business Media, 2012.
Evan Chen. Supersums of square- (SOS), 2013.
Evan Chen. A brief introduction to olympiad inequalities. 2014. URL https://weet
evanchen. haapnchen..cchanoootss/eeeggeeee
Shang-Ching Chou, Xiao-Shan Gao, and Bog--Zhog Zhang. A Deductive Database Approach to
Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 2000.
Zheng Chu, Jingchang Chen, Qianglong Chen, Weijiang Yu, Tao He, Haotian Wang, Weihua Peng. Ming Liu, Bing Qin, and Ting Liu. A survey of chain of thought reasoning: Advances, frontiers and future. arXiv preprint 200.:23099.14002 2023.
Project Coq. The Coq proof reffrece manual. INRIA Rocquencourt and ENS Lyon, ver- sion, 5, 1996.
James H Davenport and Joos Heintz. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation, 1988.
Leonardo De Moura and Nikolaj Bjømer. Efficient e-matching for SMT solvers. In Automated Deduction -CAne------- 21st International Conference Automated Deduction Bremen, Ger- many, July 17-20, 2007 Proceedings 21, pp. 183-198. Springer, 2007.
Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International Conference on Tools and Algorithmms for the Construction and Analysis of Systems, 2008
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference Automated Deduction (CADE), 2015.
DeepSeek-AL. DeepSeck-V22 V2: A strong, economical, and efficient mixture-of-expprts language model, 2024.
11

---

Published as a conference paper at ICLR 2025
Amir Dembo, Thomas M Cover, and Joy A Thomas. Information theoretic inequalities. 1EEE Transactions on Information theory, 1991.
Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023.
Zhoulai Fu and Zhendong Su. XSat: A fast floating-point satisfiability solver. In International Conference on Computer Aided Verification (CAV), 2016.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Learning to reason with HOL4 tacties. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017.
Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Proceedings of the Asian Symposium on Computer Mathematics, 2008
Google DeepMind. AI achieves silver-medal standard solving international mathe- matical olympiad problems. https:://deepmindddcc http://mmmnnn.oooooo///d////eooe slsveer/bbo/ wtt-mmm-tttiiieeee-aaa---eeeeeee
2024.
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A Formal Proof of the Kepler Conjecture. In Forum of Mathematics, Pi, 2017.
Kristian J Hammond and David Leake. Large language models need symbolic AI. International Workshop Neural-Symbolic Learning and Reasoning,, 2023.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof Artifact Co- Training for Theorem Proving with Language Models. In International Conference on Learning Representations (ICLR), 2022.
Godfrey Harold Hardy, John Edensor Littlewood, and George Pólya. Inequalities. 1952.
André Heck and Wolfram Koepf. Introduction Maple. 1993.
Marijn JH Heule, Oliver Kullmann, and Victor W Marek. Solving and verifying the boolean Pythagorean triples problem via cube-and-conquer. In International Conference on Theory and Applications of Satisfiability Testing, 2016.
Bruce Ikenaga. Techniques in proving inequalities, Sep 2018 URL https:
mi sillersville www.:eewwwbbbbaeeeeeeeeeeeeee http:////w...ooooo/ooooo/aaaaana
html
Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. Mistral 7B. arXiv preprint arXiv:2310.06825, 2023a.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. International Conference on Learning Representations (ICLR), 2023b.
Mats Jirstrand. Cylindrical algebraic decomposition-an introduction. Linköping University, 1995.
Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. ACM Communications in Computer Algebra, 2013.
Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carlo planning. In European conference machine learning, 2006.
Laura Kováes and Andrei Voronkov. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification (CAV), 2013.
Gereon Kremer. Cylindrical algebraic decompasition for nonlinear arithmetic problems. PhD the- sis, Dissertation, RWTH Aachen University, 2020, 2020.
12

---

Published as a conference paper at ICLR 2025
Gereon Kremer, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Cooperating techniques for solving nonlinear real arithmetic in the eve5 SMT solver (system description). In International Joint Conference on Automatte Reasoning, 2022.
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 Neural Information Processing Systems (NeurIPS), 2022.
Hojoo Lee. Topics in inequalittes-thheremss and techniques. Korea Institute for Advanced Study,
Seoul, 2004.
François Lemaire, M Moreno Maza, and Yuzhen Xie. The regularchains library in Maple. ACM SIGSAM Bulletin, 2005.
Kin-Yin Li. Using tangent lines prove inequalities. Mathematical Excalibur, 2006: 2005.
Zenan Li, Zhi Zhou, Yuan Yao, Xian Zhang, Yu-Feng Li, Chun Cao. Fan Yang, and Xiaoxing Ma. Neuro-symbolic data generation for math reasoning. Advances in Neural Information Processing Systems, 77:23488-23515, 2025.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su. Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, In Conference on Language Modeling (COLM), 2024.
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07644. 2025.
Nelson Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. Lost in the middle: How language models use long contexts. Transactions of the Association for Computational Linguistics, 2024.
Yang Lu. Practical automated reasoning on inequalities: Generic programs for inequality proving and discovering. Asian Technology Conference in Mathematics, 1998.
Yi-An Ma. Yuansi Chen, Chi Jin, Nicolas Flammarion, and Michael I Jordan. Sampling can be faster than optimization. Proceedings of the National Academy of Sciences (PNAS), 2019.
Radmila Bulajich Manfrino, José Antonio Gómez Ortega, and Rogelio Valdez Delgado. Inequali- fies: a mathematical olympiad approach. 2010.
Aaron Meurer, Christopher Smith, Mateusz Paprocki, Ondfej Čertík, Sergey Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. SymPy: symbolic computing in python. PeerJ Computer Science, 2017.
Michat Moskal, Jakub Eopuszański, and Joseph R Kiniry. E-matching for fun and profit. Electronic Notes in Theoretical Computer Science, 198(2):19-35. 2008.
Yurii Nesterov. Introductory lectures convex optimization: A basic course. 2013.
Allen Newell and Herbert Simon. The logic theory machine-a complex information processing system. IRE Transactions on information theory, 1956.
Xinpeng Ni, Yulun Wu, and Bican Xia. Solving SMT over non-linear real arithmetic via numer- ical sampling and symbolic verification. In International Symposium Dependable Software Engineering: Theories, Tools, and Applications, 2023.
Lawrence C Paulson. Isabelle: A Generic Theorem Prover. 1994.
Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selec- tion for Lean. In International Conference Automated Reasoning with Analytic Tableaux and Related Methods, 2023.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arX 2009x:2009.03393 2020.
13

---

Published as a conference paper at ICLR 2025
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and llya Sutskever. Formal Mathematics Statement Curriculum Learning. In International Conference on Learning Representations (ICLR), 2023.
Daniel A Roberts, Sho Yaida, and Boris Hanin. The principles of deep learning theory. Cambridge University Press Cambridge, MA, USA, 2022.
Stephan Schulz. E-a brainiac theorem prover. Al Communications, 2002.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving Lean. arXiv preprint arXiv: Arxiv-2404. 12534, 2024.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. In Conference on Language Modeling (COLM), 2024.
Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 2024.
Nguyen Duy Tung. 567 nice and hard inequality. htttss://phantuurkihh. wordpress. com/ 2012.
pdf April
Ali Uncu, James H Davenport, and Matthew England. SMT-solving induction proofs of inequal- ities. arXiv preprint arXiv:2307.1670) 2023.
Marcell János Uray. On proving inequalities by cylindrical algebraic decomposition. In Annales Universitatis Scientiarum Budapestinensis de Rolando Eotvos Nominatae. Sectio Computatorica, 2020.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jifí Vyskoëil. MaLARea SGI-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, 2008
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Eukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Neural Information Processing Systems (NeurIPS), 2017.
Pauli Virtanen, Ralf Gommers, Travis E Oliphant, Matt Haberland, Tyler Reddy, David Courna- peau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, al. SciPy 1.0: fundamental algorithms for scientific computing in Python. Nature methods, 2020.
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, al. DT-Solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Annual Meeting of the Association for Computational Linguistics (ACL), 2023.
Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without hu- man demonstrations. In Neural Information Processing Systems (NeurIPS), Datasets and Bench- marks Track, 2024.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Neural Information Processing Systems (NeuriPS), 2022.
Max Willsey, Chandrakana Nandi, Yisu Remy Wang. Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. egg: Fast and extensible equality saturation. Proc. ACM Program. Lang 5(POLL), January 2021. doi: 10.1145/3434304,
Wolfram Research. mathematical
Mathematica, version 14.1.
URL
com/
Wolfram Research. Cylindrical Decomposition, 2020. httpo//eetsss///eeeeeeeeeee wolfram..
comm//aangnaage/ref////ginniiiio Dew.oooooooaaaaeoooooooocooooco. on html
14

---

Published as a conference paper at ICLR 2025
Wen-tsün Wu. On the decision problem and the mechanization of theorem- dheorem-proving in elementary geometry. In Selected Works Of -sun Wu, pp. 117-138. World Scientific, 2008
Yuhuai Wu, Albert Q Jiang, Jimmy Ba, and Roger Grosse. INT: An inequality benchmark for evaluating generalization theorem proving. In International Conference on Learning Repre- sentations (ICLR), 2021.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Pront Prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405. 14333, 2024a.
Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. LEGO-Prover: Neural theorem proving with growing libraries. In International Conference on Learning Representations (ICLR), 2024b.
Kaiyu Yang. Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song. Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval- -aggmeet-d language models. In Neural Information Processing Systems (NeurIPS). 2023.
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AL arXiv preprint arXiv:2412. 16075, 2024.
Lu Yang. Recent advances in automated theorem proving on inequalities. Journal of Computer Science and Technology, 1999.
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.0334 03847, 2024.
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Cezary Kaliszyk, and Josef Urban. Online machine learning techniques for Coq: comparison. In International Conference Intelligent Computer Mathematics, 2021.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-Based Demonstration Learning for Formal Theorem Proving. International Conference on Machine Learning (ICML), 2024.
Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. Transactions on Machine Learning Research (TMLR), 2024.
15

---

Published as a conference paper at ICLR 2025
A
SYMBOLIC METHODS vs. NEURAL METHODS
X2
Initial goal (to be proved)
0b fas
Tactic1
Cauchy-Schwar
Intermediate goals'
(2s +2'' +
Tactic2
AM-GM
Intermediate goals"
(2a + + 22
X1
Tactic3
Simplification
Final goal (trivial)
(a) An example of CAD
(b) Incquality proving process
(c) An example of proof
Figure 6: Figure (a) demonstrates how CAD is performed on two intersecting unit circles, deriving
multiple sign-invariant cells (i.e., colored region). Figure (b) illustrates the process of inequality proving, which constructs chain of proof goals by iteratively applying tactics; Figure (c) provides a corresponding instantiation of proving ab + + ca S + 12 +
Figure ((a) illustrates how symbolic methods work in proving inequalities. Symbolic methods based on the CAD algorithm, which divides the underlying space R" into multiple connected semi- algebraic sets. In each cell, the sign of every polynomial remains constant (positive, negative, zero). T'errefore, we just need to sample one point to determine the satisfiability of each cell, rather than scanning the whole R" space. One can refer Covinness & Johnson (2012) Arnon al. (1884); Jirstrand (1995) for more details of CAD algorithm.
Figure 6(b) and 6(c) illustrate commonly used paradigm in inequality proving. In a nutshell, theorem prover often starts with the proof goal, and then iteratively transforms it into simpler form until the final version can be easily confirmed. This approach has two main advantages. First, ensures that the resulting proof can be more easily formalized in formal languages such as Lean. Second, since the hypotheses involved in inequality proofs are often straightforward, scaling and rewriting the proof goal is typically more efficient.
B PSEUDO CODE OF LIPS
Algorithm outlines the overall process of LIPS proof generation. The detailed steps for tactic generation and pruning provided in Algorithm while the specifics for goal filtering and ranking are described Algorithm
Algorithm Tactic generation and pruning of LIPS
Input: A proof goal g: A lemma library of scaling tactics t and a prompt set of rewriting tactics Vr A language model M.
Output: Tactic set T'
Initialize the tactic set T 0
2: for in + do
Scaling tactic generation
3: Obtain arguments of the tactic i using pattern_ match on the goal 4
4: Check the tactic i (with derived arguments) via the symbolic solvers.
5: if no counterexamples exist then
D Tactic pruming Solver update
6:
Add the tactic t into the tactic set T.
7:
else
8:
Update the symbolic solvers by including newly detected counterexamples. end
9:
end for
11:
for in V/ do
> Rewriting tactic generation & pruning
Obtain arguments of the tactic t by prompting the LLM.
13: Add the tactic t (with derived arguments) into the tactic set T.
end for
16

---

Published as a conference paper at ICLR 2025
Algorithm 2 Goal filtering and ranking of LIPS
Input: A goal candidate set f2.
Output: ranked set S2'.
1: Initialize a new goal set 92' O.
2: for in fl do
Symbolic goal filtering
3: Compute the homogeneity and decoupling 3 for g.
4: Define the average score the goal by (a + 3)/2.
5: end for
6: Prompt the LLM to rank the first ten goals S
Neural goal ranking
7: Obtain arguments of the tactic by prompting the LLM.
8: Re-rank the goal set Ω! according to LLM's responses.
Algorithm Overall proof generation process LIPS
Input: A formal inequality problem go: A lemma library of scaling tactics & and a prompt set of rewriting tacties V A language model M.
Output: A formal proof or timeout.
1: Initialize the candidate goal set Ω {go}-
2: for i -I...., do
3: Select the first goal g in S for exploration.
4: Obtain the tactic set T by applying Algorithm T on the current goal
5: for in T do
Tactic application
6:
Apply the tactic to the current in Lean, deriving a new goal g'. 7: Add the new goal g' into the the candidate goal set f2.
8:
end for
9: Update the goal set by applying Algorithm
10: end for
C ADDITIONAL DETAILS FOR EXPERIMENTS
The experiments conducted four Linux servers equipped with 4 Intel(R) Xeon(R) Platinum 82801. CPU @ 2.80GHz. Fach server ran Ubuntu 22.04 with GNU/Linux kernel 6.5.0-1015-azun Each proving task was performed within docker sandbox, utilizing 192 assigned CPU cores.
Neural provers. For DSP, we directly use the official code, and adapt it to Lean language and GPT-4o (version Azure-05-01). MCTS is implemented based classic upper confidence bounds applied to trees algorithm (Kocsis & Szepesvári] 2006). The value function is defined as f())) Uy + Co/log(No)/To,, where ng is the number of the proof goal á is selected and explored, No represents the number of ø's parent represents selected and explored, and C hyperparameter C /2. For the average reward Us of the proof goal Φ, use the heuristic function as Wei et al. 22044 which calculates the maximum depth of the expression trees on both sides.
Symbolic provers. For CAD, we utilize a portfolio including a suite of solvers, i.c., Z3, CVCS, RC-CAD, and Bottema. It will claim the problem is successfully proved if any one of four tools outputs unsat, and vice vica. Among four tools, Z3 and CVC5 are two popular SMT solvers; RC- CAD refers to the Bottema a CAD-based inequality prover developed by Yang [1999 As to MMA, we integrate two commands, i.e., Reduce and FindInstance in Woltram-Mathematicn (version 13.0.1), and apply the same peripheral logic with CAD.
function in Maple 2024 RegularChain package
LIPS. In framework, the symbolic solver employed for pruning scaling tactics also consists of solvers Z3, CVC5, RC-CAD, and Bottema, complemented by a numerical optimizer grounded in SeiPy (Virtanen al., 2020). The time limit of searching counterexamples is seconds. Scaling tactics encompasses a comprehensive array of inequality lemma, including AM-GM, AM- HM, Cauchy-Schwarz, Power Mean, Chebyshev, Muirhead, Jensen, Titu, Schur, Holder inequalities,
17

---

Published as a conference paper at ICLR 2025
well selection of valuable inequalities contributed by Lászió Kozma To facilitate their application in Lean 4, we have developed multiple variations of each inequality, accounting for different numbers of variables and directions. Figure 7 illustrates scaling tactics using two- variable AM-GM inequality.
theorem NEQ AM left 2vars (u v right R) (hk 2 0) (h :
(u + V 2) 2 I right) : & (u vi + is right == by
suffices (u v) positivity
2 by miinarith
theorem NEQ_AM AM GM AMM_aMMMMMMg_M___..
(u v k left : R) (hk : : 2 0)
(h left
2 k (u *
v)
+ 1) left & k (a 2 2) = by
suffices (u v positivity
2 22 by miinarith
Figure Two examples of AM-GM inequality encoded as scaling tacties
Prompts of Rewriting Tacties Generation (Simplification)
### Task
Your task is to use the condition {condition], rearrange and rewrite the expression given by the user into an absolutely different form. ### Notice
1. Please reason step by step
2. Only four operators, add, sub, multiply, and division, can be used, and should NOT introduce variables
3. Put the final results within ((boxed( e.g. \boxed {x 1/y - 2}}
### Response
User:
{problem} }
Assistant:
Prompts of Rewriting Tacties Generation (Others)
Task
You should rewrite the incquality given by the user according to the rule {rule}
### Notice
Please reason step step
Follow the given example, and output result for the given inequality
3. Put the final results within (/boxed{ ()), e.g., (\boxed (x 1/y 2)}
### Example
User:
(example. mxxample.problem)
Assistant:
fexample_answen
### Response
User:
{problem}
Assistant:
Figure 8: Prompts of simplification and other operations used for generating rewriting tactics
For rewriting tacties, we design 16 relevant operations, i.e., simplification w/o assumptions, sim- plification w/ assumptions, completing the square, variable substitution, expression expansion, pression rearrangement, expression multiplication, cancellation of denominators//umerators can- cellation of powers, extraction/cancellttio of common factors, separation/redductoon of fractions, sum-of-squares trick, and tangent line trick. Except for the sum-of-squares trick and tangent line trick implemented based on SymPy, we use two prompt templates for these operations, shown in Figure For each operation, we repeatedly query the LLM three times to cover more rewriting tac-
ittpa://wwx. wttpmmannet//teggeeee wtt.teeeeaaaaaaeeeeeeeeeee teneet//eee.git neq.pdf
18

---

Published as a conference paper at ICLR 2025
tics. We a Low-temperature setting of GPT-4o in rewriting tactic generation and neural ranking (T=0.1, top-p=1.0, max.token=2048).
D ABLATION STUDY
300
CAD
CPU time in seconds
CPU lime in seconds
240
120
60
20
15
20
25
0
10
15
20
25
30
Solution number
Solution mumber
Figure 9: CPU time vs. solution count curves of CAD and MMA. The results show that symbolic solvers can verify the inequality less than five minutes. For other problems that cannot be verified quickly, allocating more time does not improve the results. In addition, it is important to note that symbolic solvers are unable to construct human-rcadable proofs for the problems.
Scaling tactics. Figure (aa has shown how the performance on the ChenNEQ dataset (Y-axis) changes increase the number of lemmas used by scaling tactics (X-axis). When X (without scaling tactics), only 3 out of 41 theorems can be proved, whereas LIPS can prove 39 theorems.
Rewriting tactics. We observed that the successfully proved 3 theorems without scaling tactics are achieved by two rewriting tactics, sum-of-squares and tangent line trick. Hence, we further investigate the ablation of these two tactics. We newly evaluated LIPS w/o sum-of-squares and tangent lines on ChenNEQ. Among the 39 out of 41 proved inequalities, none of them requires -um-of-squares, and 3 requires the tangent line trick.
Symbolic filtering. Figure 4(b) has shown how the performance on the ChenNEQ dataset (Y-axis) changes as we increase the size of the filtered set (X-axis). smaller means more aggressive symbolic filtering. When X is large, e.g., 32, the performance drops under 40%, highlighting the importance of symbolic filtering. We did not test values of beyond 32, as this consistently caused GPT-4o to hit the maximum token limit (set at 4096).
Neural ranking. Figure 5 presents an ablation analysis where neural ranking is replaced with ran- dom selection. The results on ChenNEQ demonstrate a significant drop in LIPS performance, from 95.1% to 41.2%, underscoring the necessity of neural ranking. Additionally, we incorporate new ablation analysis that examines the effect of replacing neural ranking with purely symbolic filtering. The success rate decreased to 43.9%, indicating that symbolic filtering cannot determine an accurate proof path.
Symbolic solvers. To explore the performance of symbolic solvers, we use the ChenNEQ dataset and plot the CPU time solution count curves on Figure solvers are very fast, they can verify the inequality in less than five minutes; (2) for other problems that cannot be verified quickly, allocating more time cannot improve the results. also means that we only need to set a small time limit for symbolic solvers in LIPS.
be observed that (1) symbolic
Table 2: LIPS proving success rate if different time budgets
Method
<10min
<30min
55min
<70min
<90min
LIPS
5%
15%
35%
60%
80%
As to the results of LIPS, list the success rate CPU time in Table Additionally, plan to further enhance the efficiency LIPS in the next version, for example, by optimizing the SymPy patters en matchi ng function.
19

---

Published as a conference paper at ICLR 2025
E
CASE STUDY
A Failed Case of DSP
Prompt: Draft informal solution similar helow. The informal solution will be used to sketch
formal Lean proof. Here some examples:
Example:
Informal:
(8 ### Problem (Problem-1) }) ### Solution (Solution-1) | *)
Informal:
### Problem (Problem-2) 2} #*# Solution {Solution-2] *)
Informal:
(* ### Problem
if a, b, are positive real numbers, then
b
2
2+1 1 a++1
b
12 +1
2 +1
Informal solution:
###f Solution
We will the AM-GM inequality which states that for non-negative real numbers æ and y. the arithmetic mean is greater than or equal to the geometric mean: ?
z+v 2 Vay.
First, let's consider the terms on the left-hand side one by one and apply AM-GM to each term along with its corresponding term the right-hand side.
For the term and corresponding term
+2+1 8
we apply AM-GM to & and
+ "
11
a²
+1
2
a
1
+1
Repeating this process for with v
61+1 c2+1
and with
c2+1
obtain:
a241
+
+
2+1
1
+1
2
c²
+1
and
21
c +1
2
a² +1
Adding these three inequalities together, get:
a (6
2
82
b
+
2 b+1
V
R+
+
c+1
Notice that the left-hand side contains the terms
+ - and additional terms. Since 2+1 +
2211 12-1 0 (because all terms positive), drop these additional terms strengthen the inequality:
2+1
F+11 V
a2
Thus, have shown that the original incquality holds for any positive real numbers a, b, c.*)
Prompt:
Translate the informal solution into a sketch of the formal Lean 4 proof. Add 'suggest.tactics in the sketch whenever possible. tsatgest will be used to call the automated thearem prover. Here some examples:
Example:
Informal:
(+ ### Problem
(informal problem)
#### Solution
Linformalssolutonn }
20

---

Published as a conference paper at ICLR 2025
Formal:
probmel *)
Informal:
(* ### Problem
(informal {
### Solution
{informal 3olution
Formal:
Formal solution:
import Mathlib, Bathlib.Data..ee. Real. Beal.
import Mathlib, Iactic, Linarith Linaii.
import Mathlib. haw.ii...acccc..sssssttaaaeee
theorem inequality_amg, (a b R) (ha : a) (hb : 0 < b) (he
: 0 < c) (a b)
+ (c >
(sgrt (1a"2 + 1) / (b"2 1)1) (sqrt (lb22 1) (c 1))) (sqrt (1e22 + 1) (a 1))) :-
by
-- Apply the Arithmetic Mean-Geometric Mean Inequality (AM-GM) have gm ab real.am gm / b) 11b22 1) a),
have am gm be := real. am gm (b c) (1e22 + 11 b),
have am gm ca := real. seal.am_ga gm (c a) ((a"2 + 1) c),
The AM-GM inoquality gives the following: b (b 1)
am..mmaa :
/ 2 sgrt ((a b)
((b22 1) / a
jmm_g__c : (b / c (c + 1) / b) / 2 sqrt ((b / c)
((c²2 / b]]
am ammgm__a :
a (a*2 1) / sqrt ((c
(1a"2 1) / c)
- Now, sum the three inequalities: linarith [am_gm_ab, am_gm_bo, am_gm_cal,
Simplify the right-hand side to match the terms of the original inequality
snngestt_acttis could assist in automating algebraic simplifications here:
suggest
Conclude the proof using positivity of additional terms Positivity of terms like (b 1) / and others should be straightforwars
have pos_terms : (b + 1) a (e + 1) b (a 1) / > 0, apply add pos, -- breaking it down into multiple positive parts all goals apply pos; linarith I,
Dropping the additional positive terms from the left-hand side to strengthen the inequality linarith [pos_terns],
### Explanation the Steps:
1) Initial Setup and Imports: We start by importing necessary modules from Mathlib, such as basic real number operations and the linarith tactic for linear arithmetic.
Statement the Theorem: The theorem inequality -ammm stated three positive real numbers
a, and c. The assumptions ha, hb, and he enforce the positivity conditions.
3)
###li Conclusion
This sketch outlines the formal structure of the proof highlights where automation can assist.
21

---

Published as a conference paper at ICLR 2025
Failed Case of OpenAl -preview
Prompt: Please solve the following problem: For 0, 0, 0, such that b+
c. d d show that:
a²
b3
d+a+b a+b+c 2
b+o+d d c+ a
Informal solution:
To solve this problem, we aim to show that for positive real numbers a, b, c, d satistying ab + be + od + da = 1, the incquality
B b+c+d" c+ a d
e
df atb+e
holds true.
Step 1: Simplify the Inequality. First, note that
b + = a,
where = aabbect Thus, inequality can rewritten as:
Σ
S
cyclic
Step 2: Analyze the Function. Consider the function
f(x)
x E (0,
We will investigate the convexity of this function to apply Jensen's inequality. Compute the second derivative:
25 + 28x x² > 0 for x x (0,
(x)
(S x)3
This shows that o f(x) is convex on (0, S). Step 3: Apply Jensen's 's Inequality. Since f() is convex, Jensen's 's inequality states that:
Σ f(a))
2
1
Σ a
f {(3)
4
11
1m1
Compute f (E):
(
(8)
(5)3
$2
15
48
Therefore, the sum becomes:
5
S
Σ
4
48
12
cyclic
Step 4: Relate the Given Condition. From the given condition ab + be + od + da 1, and using the Cauchy-Sehie Schwarz inequality:
(ab + ed + da) S 2
(a²
2 +
But since ab + be + ed + da 1. we get:
2 + 2 + 8 22
Also, note that
(attbbt
2 2 4(0² 4 8
4
8,
so s0 28.
Therefore:
Σ
2
8
2
12
12
3
gyllic
22

---

Published as a conference paper at ICLR 2025
But this contradicts the desired inequality, suggesting miscalculation.
Step Test the Equality Case. Consider a d = 2.2 Then:
ab be + ed + do 4 ( 1 =
Compute left-hand side:
Σ + + 4
1 2 8
This shows that equality holds when a = == d Step 6: Conclude the Proof Since the function (x) is convex. the minimum of the when all variables are equal, i.c., a = b ==== d. Therefore, the inequality holds true:
1 b+o+d ctd+a dtatb a+b+c 2 3
ba
Failed Case of LIPS
Problem (USAMO 2004): Let a, b, c positive reals. Prove that (a + b b+
c)²
S (a a² + 3) (b5 b2 + 3) (c
6²
+ +3)
Formal solution:
theorem Problem 3dP5 la b o: R1 (ha : a 01 (bb
b
(hc
> 0) (a ba+boon b 3 < (a
3) (b
5 b
3) (c - 2 + 3) := by
scale NEO
laarz_leet__aa_ 3vars (ul 1) (u2 1) (u3
:= (vl a)
(v3 := c)
scale NEQ [e00_weighted__1 AM_ La__GM_let___tee 3vars (u 1- + c) (v := 3) (M
:- a + b*2 222) (il :- 1) (12 : 1/2) (:3 : 1/2)
11m fim_frac_reduee
Lim_eancel_dene
scale NEQ Scwwaaaausaaaaraaccaaaaa wwwwwsswwweeeeeeeeeeeweeeaeeeeea setwarrzssgt_lett 2vars (ul 1= 1) (u2 1) (vl
a) (v2 :- a)
11m_simplify...
1lm_rearrange
1lm_simplify
1im_rearra
1lm_simplify
1lm_rearrange
1lm_frac_apart
llm_simplify
1lm_rearrange
11m_frac_apart
11m_simplify
iim_simplity
rearrange
11m iim_simplify
1lm_rearrange
1lm_simplify ...
llm_factor ... 4*sqrt ssrt (b + c3 a 6 c.2
+ 2+a 2+b 2xc) 2 (1 a) 23 + a b-2
2 2+8 +
2+b + 2xc) 22 (64x (3 + a a32)) + 555 bb2)) 5
c22))
FAIL (TIMEOUT)
23

---

Published as a conference paper at ICLR 2025
Successful Case of LIPS
Problem (Evan Chen): If ra, b, e positive reals and a² 17 c² 1, then
1
+
+
+
a
+2
62
+2
22
6ab c
6bc a²
6ca + 82
Formal solution:
theorem Problem 2d4e1 la b о > 0) (a : a
R1
(ha
: a
0)
(bb
0)
the : + 1
2 + +
11
1
[a "
2 +
21
(o 2 2 2) + (c 2
2) S
(6
t b
21
+
(6 b
2) + +
2)
by
scale
(u
1- b) (V : 6)
scale NEQ AM wtt.dii_ssaarreerggttttoooooooot 2vars
(u := b) (V := a)
scale NEQ AM am_div__sparr_riihtt... 2vars
(u := a)
(V := c)
11m_simplif
1lm_simplify ...
lim_rearrange ...
sym_tangent_ aawaannnnttiinneeee
11m_simpl Fy 27/49 227.2"//49) - (27+b"2/49) (27xa 2/499) try close
SUCCKSS!
F
SOME MORE CASES OF LIPS
Different Proof Generated by LIPS (1)
Problem:
Let o, b, c be three positive reals. Prove that if abc = 1, then
a² + 1/2 z
Source: http://///aa...aaaaacccc/coooaaa
Formal solution:
theorem Example_1d {a c R]
(h := by
1) faab+os
a 2 + b 2
scale NEQ AM_ GM Le__MM__ftt__uuureeeeeo 2vars
(u 1)
scale NRQ_AM_GM_166 wtw____leett_ssurre_eeP_
(u :- 1) (V :
scale LaL_AA_G___eet__surrrra
(u :- 1) (v :- b)
11m_rearrang, 11m slm_simplity
3/2 - a 2/2 b'2/2 622/2
11m rearrange (left 3/2) (right a"2/2 222 c22/2)
scale NEQ AM GM right normal 3vars (u i= 222/2) (v b22/21
1lm_simplify 1lm_simplify try close
(a+bee) 2
1 /
Note: At first glance, "AM-GM alone hopeless here, because whenever we apply AM- GM, the left and right hand sides of the inequality all have the same degree". However, LIPS
find a proof by using 1 2++ 1 1xbs R+1 1 1xcss= 1 1+1
24

---

Published as a conference paper at ICLR 2025
Different Proof Generated by LIPS (2)
Problem (JMO 2012):
Let a, b, positive reals. Prove that
a 5b
ba +c
c² + 5a
3c - a - 2
+
3a 6
3b+c
Source: http:////.....o..........//////a
Formal solution:
theorem Froblem 3d 0 0) :
R]
(ha
(bb
0) (he
21 (a
21
(a
3) / (3
b)
(b
c 3)
13
5
6) +
(c 3
a 3) / (3 +ot00 :- by
11m_cancel_facton
scale NEQ_Mui sheaddireeddd_neettee Baiee__rrgtt__aarr__ 3vars
1- a)
(v :- b)
scale NEQ Muirheadl left 3vars (u := c) (V 1= a)
(w := b)
scale NEQ Muirheadl Leiteaddl_eef____1
1eat_3vars 3vars (u := a) (v 1= b)
(w 1= c)
scale NEQ Mww.hhead__onsteeeeeee leas_3vars (u 1= a)
left 3vars
(v b)
l_m_cancel_factor ...
scale NEQ Ntp_MMulhccae_onnetttrrggggggg 3vars
a) (v := b)
1lm_simplify scale 2tt_MMirrhead2_eft___33
(u : c) (v : b) (x : a) Note: A completely mechanical proof, achieved by iteratively applying Muirhead inequality six times after canceling the denominator
LIPS Checks Existing Answers (1)
Problem (Japan 1997): Prove that
(b + c a)²
(c+ a 6)
(a 1 c)² (a a b)
3
(b (b+c)² +
(c+ a)² +
+ c
Source: http:///aa..a.oooooaaaaaaaaaaaaa
Informal solution No.1 (provided by AoPS community):
Solution:
Let:
P (b)--a)2 + (0+
(6+a)=462 + (a+b-e))
(a+6)*+oz By Cauchy Swarchz inequality, have
b2 +2 (0----
(a+b+
(3(a² + +0)++++))))+ (a+boo)))))))
(3 4(ab be be (a+boof
Hence,
P 3[atbte) bcb+bcta but we know that (a + b c)2 > 3(ab + be + ca),
(atbte)²
P b(ab+be-ca)-
beatbbctca)
the proof correct all variables are assumed to be positive. However, without this assumption, applying Cauchy-Schwarz is incorrect, and counterexample successfully found by our symbolic solver [c = 8.0, a = 1/8, b = (-1.0)]
Note:
This problem proved by LIPS using Il iimssippiiiiattion and tangent_ line trick tacties.
25

---

Published as a conference paper at ICLR 2025
LIPS Checks Existing Answers (2)
Problem (Japan 1997): Prove that
(b bb+c- a)²
+ (c+ 1)2
(a + b c)
3
+
2
(b+ (b+c)* + (c+ a) +
(a + b) + c²
5
Source: httr::///attffrrrrommeeeeellnino
wtw.uuuuuttyyccooo c/6 6p537
Informal solution No.2 (provided by AoPS community):
don't use much of mathematics on that simple problem..
:P :D here's the solution using TITU's lemma.. The lemma-
v, y, a, are reals and v; y > 0 then a² 82
(z+g)
simply applying the lemma on the Ihs twice get
LHS 2 31a (a+b+c)²
by AM-GM
(a (a+b+e) 2 3(ab bc ca) and 3(a² + 62 +c²++ 2(ab + be + ca) > 5(ab + be + ca)
Note: it appears that the issue arises from the inequality being in the wrong direction. Ac- tually, the problem unprovable when applying the Titu's lemma counterexample found by our symbolic solver: [b 1.0, a = 1.0, = 0.5))
26


Reviews:
[{"review_id": "eDdCTL7XzC", "reviewer": "Reviewer_4dY9", "summary": "The paper studies a neural-symbolic integration method, named Lips, for mathematical inequality problems. The paper first identifies the two key tactics in inequality problems, scaling and rewriting. Application of the scaling tactic is determined by a symbolic method, and application of the rewriting tactic is by prompting an LLM. Applying these tactics creates new proof goals, and the paper filters the created goals by a symbolic method and scores the surviving ones by prompting an LLM.", "questions": "- How influential on the performance are the symbolic-based transformation tactics, sum-of-squares and tangent line tricks? In other words, what happens if only neural-based transformation is applied?\n\n- What are the up-arrow and down-arrow in the caption of Figure 3?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "+ Solving mathematical inequalities is a challenging, and significant task. It also has application to formal verification.\n\n+ The proposed approach is a nice integration of symbolic and neural methods. The criterion to distinguish between their use in tactic application is clear: reasoning in a finite search space is conducted symbolically and reasoning in an infinite space is neurally. The idea of symbolic filtering and neural scoring is natural, but its significance has been (partly) proven in the experiment.\n\n+ The experiment evaluates the performance of the proposed approach and the potential with respect to the improvement of the underlying LLM. Both are promising.", "weaknesses": "- I don't think this is a weakness of the current form of the work, but the paper could enhance the work and broaden the audience if it can claim there are other math domains with two types of tactics such that one is suitable for symbolic reasoning (or the search space of its application is finite) and the other is for neural reasoning (or its search space is infinite), like scaling and rewriting in inequality problems.\n\n- Some parts of the proposed approach are unclear (see the following questions).\n\nOther comments:\n\n- l296: In the definition of HM, the correction of the second occurrence of $d_i$ may be $d_j$.\n- I think, after calculating the decoupling score and homogeneity score, only top-k candidates are selected (in the experiment, it seems that only top-10 candidates remain), but it might be nice to clarify it in Section 4 (I noticed it during reading Section 5.1).\n- The caption of the right figure in Figure 4 is a bit confusing. Rephrasing it to, e.g., \"Various sizes of filtered goal sets\" may be helpful.\n- For RQ2, the paper says a direct comparison of proving time could be unfair, but I'm not sure whether only comparing the pruning ratio of scaling tactics and the number of iterations in goal selection is fair. Even if the pruning and goal selection are improved over a long period of time, it may not lead to improving the performance of the prover itself. I'm wondering that showing all the comparisons of proving time, pruning ration, and the number of iterations in goal selection may be more fair.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "FmD02iAehc", "reviewer": "Reviewer_cEd1", "summary": "The authors introduce LIPS: a hybrid system for proving inequalities, which combines symbolic solvers, manually crafted heuristics, and   LLMs. LIPS operates within the formal framework of Lean 4. The system is evaluated on a test set of 161 competition-style inequalities of varying difficulty, and is compared to 5 other methods (2 purely symbolic and 3 ML-based). LIPS performs significantly better than the baselines on the considered test set given the time limit of 90 minutes.", "questions": "1. Could you provide the Lean and SMT formalizations of the test inequalities?\n2. Could you provide the implementation of LIPS?\n3. What precise parameters were used for SMT solvers to obtain the CAD baseline? \n4. How is MCTS implemented? Do you apply symbolic filtering during the search, similarly as in LIPS?\n5. Why do you write \"Please reason step by step\" in the prompts for neural ranking? What are the full resulting responses from GPT-4o? \n6. What is meant by \"iteration of LIPS\" in Figure 3? And what is an \"iteration\" in the oracle? How do you obtain the oracle proofs?\n7. How does search work in LIPS? Is it best-first search? Or breadth-first search?\n8. In line 412 you write: \"LIPS outperforms the existing method in 13 out of 20 problems\". I cannot see this in Figure 3, could you explain?\n9. When you do neural rewriting, how do you verify that the rewrite is correct?\n10. You use SymPy's `simplify` to compare with \"neural\" rewrites. What does this function do? \n11. Did you consider to use simpler ML techniques in place of GPT-4o? \n12. What would happen if you get rid of the neural ranking and use solely homogeneity and decoupling metrics to rank the goals? \n13. You write: \"Our techniques could serve as a solid foundation for broader areas of mathematical research such as\ninformation theory, optimization, and deep learning\". Could you explain a bit how?", "limitations": "", "rating": 5, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "The work demonstrates the potential of combining machine learning and symbolic/formal techniques, which is an interesting and still under-explored direction.\n\nThe design of LIPS looks well thought out, leveraging appropriate symbolic techniques in the pipeline.\n\nThe authors compared LIPS against a representative variety of baselines, both symbolic and ML-based.\n\nThe paper is mostly written clearly, and provides enough background information and helpful examples (but some parts are less clear -- see weaknesses below).", "weaknesses": "The test dataset is not publicly available. In particular, the Lean and SMT formalizations are not available. It is relatively easily to introduce unintended errors when formalizing math, so open-sourcing the formalizations is important to make inspection possible. Also, it is crucial to allow other researchers to compare their approaches by providing the test data.\n\nThe implementation of LIPS and MCTS is not available for testing and inspection, and there is no promise of open sourcing it. \n\nSome parts of the description of LIPS are unclear to me -- see questions below. In particular, it is described how LIPS generate a set of new proof goals from one proof goal, but the main body of the paper does not contain any information on how search is conducted in the resulting tree of proof goals.\n\nThe related work section is missing important related literature. Combining formal theorem proving with machine learning is not limited to LLMs. There is a rich body of research combining other ML approaches and proof assistants [1,2,3,4,5]. It is very well possible that more light-weight ML approaches would be more suitable as non-symbolic components of LIPS.\n\nThe evaluation is somewhat limited and unconvincing. \n- It would be informative to see a \"time limit vs proof success rate\" plot in addition to the table showing the stats for the 90 min. time limit. This limit is rather high, and I suspect that the symbolic approaches, when they solve an inequality, they do this within the first couple of minutes.\n- It is possible that the improvement achieved by LIPS compared to CAD-based approaches is due to the set of carefully handcrafted scaling lemmas that fit the test problems. Also, it seems that the size of the filtered set was selected to fit the test problems best, and there was no separate validation set to fit this parameter.\n- It would be good to see more ablations: the effect of symbolic filtering; the effect of special tactics (sum of squares, tangent line). \n\n\nThe problems from the test set are publicly available on the internet, therefore GPT-4o could be trained on those. This raises a question about reliability of the evaluation of LIPS, where GPT-4o is used. \n\nTheorem proving in Lean is not sufficiently introduced, which is important given the ML-oriented audience of ICLR.\n\nThe presented approach to an extent is inspiring other combinations of symbolic and ML techniques, but LIPS as a system is very specific to the problem of proving competition-style inequalities; it may not translate to more general / practical problems in any simple way. \n\nMinor remarks:\n- The description of the X axis in Figure 4b looks to be wrong.\n- Figure 3 shows 19 problems, whereas in the text you write about 20 problems.\n- The Y axis of the left plot in Figure 3 should start at 0 not 60.\n- \"AM-GM inequality\" -- you should explain the acronym here. \n\n[1] Blaauwbroek et al.: Graph2Tac: Online Representation Learning of Formal Math Concepts. ICML 2024\\\n[2] Piotrowski et al.: Machine-Learned Premise Selection for Lean. TABLEAUX 2023\\\n[3] Zhang et al.: Online Machine Learning Techniques for Coq: A Comparison. CICM 2021\\\n[4] Gauthier et al.: TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017\\\n[5] Urban et al.: MaLARea SG1 -- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR 2008", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "GzhirjPSwR", "reviewer": "Reviewer_v6PZ", "summary": "The paper introduces LIPS, a neuro-symbolic system that combines large language models (LLMs) and symbolic reasoning to solve Olympiad-level inequality problems in formal theorem proving. \n\nLIPS divides tactics into scaling (using symbolic tools) and rewriting (using LLMs):\n\nScaling applies known inequality lemmas (e.g., AM-GM or Cauchy-Schwarz inequalities) to refine subterms in the target inequality. The symbolic approach allows exhaustive enumeration of lemma applications across potential arguments. However, only certain applications lead to correct deductions since overscaling risks invalidating the inequality. To address this, LIPS uses counterexample filtering to eliminate incorrect transformations. This involves generating possible solutions with symbolic tools (e.g., CAD solvers) to check whether the inequality holds across variable values, discarding transformations that fail.\n\nRewriting tactics focus on algebraic transformations to express terms in alternative but equivalent forms. This space is vast (infinite transformations possible), so LLMs are employed to guide the selection, generating transformations that preserve provability. LIPS designs prompts for common transformations (e.g., factorization, denominator simplification), allowing the LLM to filter likely useful transformations.\n\nThe authors conduct evaluations on 161 challenging inequality problems and demonstrate their system is significantly more capable than existing systems.", "questions": "- Can you describe how the Lean 4 commands such as `llm_simplify`, `llm_rearrange`, etc. do? It would be great if you could provide a complete Lean 4 code that people can run for reproducibility and verification purposes.  \n- It would be interesting also to compare to existing Neural Theorem Provers in Lean 4 such as DeepSeek Prover V1.5 or LeanCopilot.", "limitations": "", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "The paper takes a novel approach (to my knowledge) to solve olympiad inequalities following the recent paradigm shift of using test-time compute to solve mathematical problems. The domain specificity of solving inequality problems is very well exploited. The method rigorously categorizes proof tactics into scaling and rewriting, with each category handled by techniques suited to its complexity. This results in successful results as demonstrated by extensive experiments and results in proofs written in Lean 4 and hence has guarantees.\n\nLIPS sets a new benchmark for inequality theorem proving by combining machine learning with symbolic techniques, which is promising for broader applications in automated mathematics. \n\nThe paper is well-organized, clearly explaining both the technical details of scaling and rewriting, and the hybrid neuro-symbolic approach.", "weaknesses": "It is unclear to me how LLM rewritings are formalized in Lean 4 - is it a Lean 4 tactic that can do the rewrites of LLM? If that is the case, it would be interesting to use this as a tactic in general theorem proving in Lean 4.\n\nThe datasets used (e.g., ChenNEQ, MO-INT, 567NEQ) focus on specific competition-level inequalities, which might limit generalizability. I don't understand why authors took a random sample of 100 from 567NEQ instead of running the system on all of them. I think it is important to make sure that there was no contamination due to solutions of these problems appearing in training data of GPT4o, although I believe the failure of other LLM based approaches is evidence that LISP's added value is significant.\n\nI believe some evaluation comparing to existing theorem provers such as the one from DeepSeek or LeanCopilot could be included. I would also love to see the code on how the LLM rewriting tactics could be formalized in Lean 4.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "WsivtpSHQk", "reviewer": "Reviewer_YrrG", "summary": "The paper presents a neuro-symbolic tactic generator designed to solve typical inequality problems found in\nmaths olympiad contests. The authors identify two general strategies often employed by humans in solving these problems, which involve creating new goals via:\n- Scaling, which involves the application of known lemmas, inequalities, etc., to the inequality that needs solving.\n- Rewriting, which involves using common equivalent transformations on the inequality that needs solving.\n\nLips utilises a blend of symbolic methods, used for scaling and some rewriting, and LLMs, primarily used for rewriting inequalities and ranking and selecting goals. The performance of Lips is compared with state of the art tools on common benchmarks. Additionally, general paradigms for neuro-symbolic reasoning are extracted from the approach Lips takes for math olympiad inequality problems.", "questions": "- As mentioned in my weaknesses, I remain unconvinced about the broader impact of this paper beyond \nthe neuro-symbolic resolution of inequality problems. Could you clarify what the novel findings are \nin a wider context? Maybe even what are specific tasks, problems that benefit from your reasearch, aside \nmath olympiad problems? \n\n- The development of a tool like Lips could be noteworthy, but I am not familiar with similar existing \ntools. Am I correct in understanding that it is the first tool to integrate neural and symbolic components? \nIn your experiments, it appears that you only compare it to tools that are either purely neural or purely \nsymbolic.", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 4, "contribution": 2, "strengths": "- The development of neuro-symbolic tools for reasoning about formal tasks is quite intriguing, and this paper contributes nicely in that its findings seem to transcend the specific task of solving maths olympiad questions.\n- The approach taken by Lips is explained in detail and is easy to comprehend. Overall, the concept behind Lips appears sound.\n- The experimental parts of the paper are sufficiently supported. \n- The paper is well-written and organized, with everything supported by examples. \nI found it an enjoyable read.", "weaknesses": "I order the weaknesses from most to least important:\n- It is unclear to me how impactful the findings of this paper are beyond \nthe development of a well-performing neuro-symbolic tactic generator \nfor these specific inequality problems. While the workflow of Lips \nis a nice combination of symbolic and LLM-based components, the underlying \nidea seems rather straightforward: whenever symbolic methods are \nsufficient (as in the scaling steps), use symbolic; and whenever things \nbecome less clear (as in rewriting and goal selection), use LLM. While I \nmay be incorrect, this seems folklore to me.\n- While I appreciate the paper's lightweight tone, at times, \nit feels that many choices are justified by intuition alone. \nFor example, the authors state that scaling and rewriting are the methods humans use to solve such inequality problems. This seems reasonable to me, yet there is no evidential support for this in the paper. Similarly, in Section 4.1, the authors introduce criteria for ranking proof goals. \nAgain, these appear reasonable to me, but there is no support for these claims. \nIt may well be the case that research on such questions is simply non-existent, but I would have appreciated it being stated more clearly why we have to rely on intuition.\n- At some points, the paper's language is a bit too informal. For example, \nin the paragraph starting with line 180, it is stated that OpenAI's o1-preview \n\"cannot solve a specific inequality\". The proof presented is an example \nof a prompt given to o1-preview, where it fails to address this particular \ninequality. Clearly, this is not a sufficient argument to claim that \no1-preview is generally unable to solve such inequality tasks.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)