Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

Dear reviewer YrrG:

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns. Please feel free to follow up if you have further questions!

1. Justification for Scaling/Rewriting Tactics and Heuristics for Filtering Proof Goals

The intuition is largely drawn from notes and books written by IMO coaches. For scaling/rewriting tactics, Bruce Ikenaga summarizes in his note on inequality that ``You can often prove an inequality by transforming or substituting in a known inequality'' (source). Similar discussions can also be found on MathExchange. Regarding goal ranking, concepts such as coupling and homogeneity are frequently emphasized in references like [1, 2], which is why we incorporate them as metrics. We are unaware of existing literature studying these intuitions systematically.

[1] Mildorf, Thomas J. "Olympiad Inequalities." Preprint, https://artofproblemsolving.com/articles/files/MildorfInequalities.pdf

[2] Evan Chen. "A brief introduction to olympiad inequalities." Preprint, https://web.evanchen.cc/handouts/Ineq/en.pdf

2. Evaluating OpenAI o1

The line starting at Line 180 only claims o1 cannot solve the particular inequality problem in Figure 1. This paragraph does not claim o1 cannot solve a class of problems. However, we also evaluated o1 on the MO-INT dataset, and it wasn’t able to solve any of the problems (Line 398 and Appendix D). In contrast, LIPS solved 16 out of 20 problems in MO-INT (Table 1).

3. Comparisons with Existing Tools for Proving Inequalities

Thank you for bringing up an excellent question! To the best of our knowledge, LIPS is the first tool to integrate neural and symbolic reasoning for both tactic generation and subgoal evaluation, providing a comprehensive approach to inequality theorem proving.

Existing tools generally fall into one of two categories: (1) purely symbolic methods, such as CAD solvers, which do not produce interpretable proofs, or (2) neural-based methods, like INT [1], that rely entirely on neural networks for tactic generation and subgoal evaluation. Among these, AIPS [2] takes a slightly different approach by leveraging symbolic methods for tactic generation and training a language model for subgoal evaluation.

In contrast, LIPS conducts both tactic generation and goal ranking in a neuro-symbolic manner. Specifically, while AIPS relies on a fixed set of symbolic rewritings, LIPS particularly uses LLMs to handle rewriting tactics, allowing for a more flexible and dynamic action space, which better reflects the nature of mathematical reasoning. For goal ranking, AIPS synthesizes similar inequalities and fine-tunes an LLM to rank the subgoals, whereas LIPS combines symbolic filtering with ranking by GPT-4. Additionally, AIPS assumes the inequality problem is cyclically symmetric and tight, whereas our neuro-symbolic framework steps aside from these assumptions, providing greater generality. As a result, the neuro-symbolic design of LIPS enables it to significantly outperform AIPS in empirical evaluations.

[1] Wu, Yuhuai, et al. "Int: An inequality benchmark for evaluating generalization in theorem proving." ICLR 2021

[2] Wei, Chenrui, Mengzhou Sun, and Wei Wang. "Proving Olympiad Algebraic Inequalities without Human Demonstrations." NeurIPS Datasets and Benchmarks Track 2024

4. Suggestions on the Writing

Thank you for pointing out potential confusions! We will clarify them using more precise language in the next revision.

Thank you for following up! Below is our detailed response.

beneficial to incorporate at least an informal paragraph summarising the justifications you provided above

Thank you for your suggestion! We will incorporate the justifications into our paper.

you provided a single prompt for which o1-preview failed to solve the inequality problem of Figure 1. However, perhaps a slightly different prompt would suffice?.

Thank you for the clarification. We apologize if the original statement had caused confusion. To make the claim more precise, we will re-word it along the lines of "o1 cannot solve the inequality in Figure 1 when the problem is presented directly in the prompt".

Our prompt for o1 is

Please solve the following problem:
<PROBLEM_STATEMENT>

where <PROBLEM_STATEMENT> is the original problem statement in LaTex from the problem's original source, e.g., Chen [1] and Tung [2]. We do not define "Olympiad-description" or try to normalize the problem statement into a canonical format.

As recommended by OpenAI's official o1 prompting guidelines, a simple and direct prompt like ours will likely outperform more sophisticated prompts that employ techniques such as few-shot demonstrations or chain-of-thought prompting. Similarly straightforward prompts have been used for evaluating o1 in recent studies [3, 4].

Additionally, we newly experimented with several different prompts, including:

• Chain-of-thought prompt (“Let’s think step-by-step”)
• System prompt (“You are an experienced educator in the field of MATHEMATICS”) [5]
• A popular prompt shared on Reddit.

Despite these efforts, the o1-preview model still fails to solve this particular inequality problem.

[1] Chen. "A brief introduction to olympiad inequalities." 2014

[2] Tung. "567 Nice And Hard Inequalities." 2012

[3] Li et al. "OpenAI-o1 AB Testing: Does the o1 model really do good reasoning in math problem solving?." arXiv 2024

[4] Zhong et al. "Evaluation of OpenAI o1: Opportunities and challenges of AGI." arXiv 2024

[5] Gao et al. "Omni-math: A universal olympiad level mathematic benchmark for large language models." arXiv 2024

possible connection to SMT solvers … I would expect that neuro-symbolic approaches are already being investigated in these contexts

To the best of our knowledge, neuro-symbolic approaches have not been used to enhance SMT solvers in the specific context discussed in the common response.

SMT solvers are complex systems with many components (see Figure 1 of [1] for an overall architecture). Broadly speaking, an SMT solver integrates various decision procedures (e.g., for integers, strings, and real numbers) and uses them effectively to solve problems. Existing work has attempted to use machine learning to improve SMT from many directions, e.g., synthesizing custom Z3 strategies [2, 3], learning heuristics for quantifier instantiation [4, 5], and selecting the best solver for a particular problem from multiple solvers [6]. However, these approaches generally focus on how decision procedures are applied. They operate at a higher, meta-level, treating the decision procedures as black boxes.

In contrast, what we proposed in the common response was to potentially use LIPS to replace or enhance the decision procedure for quantifier-free non-linear real arithmetic. A related line of work uses machine learning to learn heuristics in cylindrical algebraic decomposition (CAD) [7, 8]. CAD differs from LIPS (inner workings; whether human-readable proofs can be generated; discussed in Sec. 2.1). Nevertheless, one can potentially extract intermediate inequalities from LIPS’ proof search process as data for training machine learning models to enhance CAD.

[1] Bjørner et al. "Programming Z3." Engineering Trustworthy Software Systems: 4th International School, SETSS 2018

[2] Balunovic et al. "Learning to solve SMT formulas." NeurIPS 2018

[3] Lu. “AlphaSMT: A Reinforcement Learning Guided SMT Solver”. University of Waterloo, 2023.

[4] Janota et al. "Towards learning quantifier instantiation in SMT." SAT 2022

[5] Blanchette et al. "Machine learning for instance selection in SMT solving." AITP 2019

[6] Scott et al. "MachSMT: A machine learning-based algorithm selector for SMT solvers." International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2021.

[7] Huang et al. "Using machine learning to improve cylindrical algebraic decomposition." Mathematics in Computer Science. 2019

[8] Jia et al. "Suggesting variable order for cylindrical algebraic decomposition via reinforcement learning." NeurIPS 2024

I see where you are coming from regarding the potential benefits for SMT solving, however our discussion about this remains superficial, which is partly due to the fact that I have not much background knowledge about the existing literature.

I feel my issues mostly resolved and I do not feel that I can contribute anything of worth to the rebuttal anymore. I am not fully sure about the broader impact of this work, but I acknowledge its contribution.

Accordingly, I increased my rating to a "weak accept" as I think its an overall nice contribution, but I decreased my confidence to "2" as it became clear that I could very likely be not aware of important related work.

Thanks for the nice discussion, I really appreciate the way you are handling the rebuttal!

Dear reviewer v6PZ:

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns. Please feel free to follow up if you have further questions!

1. Implementation Details of Rewriting Tactics in Lean 4

Please see our common response at the top of this page.

2. Why Using a Subset of 100 Problems from 567NEQ?

We selected a subset of 567NEQ primarily due to budget constraints. However, we plan to extend our evaluation of LIPS to the full dataset in future work.

3. Potential Data Contamination Due to GPT-4o

Please see our common response at the top of this page.

4. Comparisons with DeepSeek-Prover-V1.5 and Lean Copilot

As suggested by the reviewer, we evaluated DeepSeek Prover V1.5 and LeanCopilot on the Mo-INT dataset. For LeanCopilot, we used the default setting and apply the search_proof tactic. We observe that LeanCopilot fails to prove any problems of this challenging dataset, consistent with the result reported in AIPS. For DeepSeek Prover V1.5, we used the DeepSeek-Prover-V1.5-RL model provided on Huggingface and evaluated its performance using the Pass@32 metric. Similarly, it also fails to solve any of the 20 problems.

Dear reviewer 4dY9:

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns. Please feel free to follow up if you have further questions!

1. Comparison with AIPS in Proving Time

First, we would like to clarify that the code for AIPS is still unavailable; therefore, we have re-implemented its tactic pruning based on the descriptions in the paper. As suggested, we also evaluated proving time by replacing our tactic pruning methods with AIPS’s equality-checking approach. The results below (similar to Figure 3) show that LIPS’s pruning consistently outperforms AIPS’s on 14 out of 20 problems in terms of proving time (minutes). Moreover, AIPS’s pruning significantly degrades LIPS’ proving success rate on MO-INT from 80% to 40%.

2. Neuro-Symbolic Reasoning for Other Mathematical Domains

In LIPS, we design two types of tactics: scaling tactics are more natural for symbolic reasoning, and rewriting tactics are more natural for neural networks. This kind of structure is not limited to the domain of inequalities. One example is AlphaGeometry for proving 2D Euclidean geometry problems [1]. It uses symbolic reasoning to deduce basic geometric properties and neural networks to introduce auxiliary constructions (points, lines, or circles not present in the original problem). For a broader discussion on the generality of LIPS, please see our common response at the top of this page.

[1] Trinh, Trieu H., et al. "Solving olympiad geometry without human demonstrations." Nature 2024

3. Ablations of Sum-of-squares and Tangent Line Tricks

Please see additional ablations in common response at the top of this page.

4. Arrows in Figure 3 Caption

The up arrow ($\uparrow$) means “higher is better” (for the tactic pruning ratio). The down arrow ($\downarrow$) means “lower is better” (for the number of iterations). Thank you for pointing out the confusion. We will clarify them in the next revision.

5. Typos and Writing Suggestions

Thank you for your valuable feedback! We have revised accordingly.

Q9: When you do neural rewriting, how do you verify that the rewrite is correct?

Please see our common response at the top of this page.

Q10: You use SymPy's simplify to compare with "neural" rewrites. What does this function do?

SymPy’s simplify function automatically simplifies a given mathematical expression using heuristics. Details and examples can be found in its documentation.

Q11: Did you consider to use simpler ML techniques in place of GPT-4o?

As discussed in a previous remark, it is difficult to directly replace LLMs in LIPS with simpler ML models, due to challenges in rewriting tactic generation and zero-shot prediction.

Q12: What would happen if you get rid of the neural ranking and use solely homogeneity and decoupling metrics to rank the goals?

Please see this ablation in our common response at the top of this page.

Q13: You write: "Our techniques could serve as a solid foundation for broader areas of mathematical research such as information theory, optimization, and deep learning". Could you explain a bit how?

We meant LIPS could potentially be extended to help prove theorems from many branches of advanced mathematics such as information theory and optimization. Please see our common response at the top of this page for more discussion and examples.

Dear reviewer cEd1:

Thank you for taking the time to review our paper and provide feedback! Below we address your questions and concerns. Please feel free to follow up if you have further questions!

1. Data and Code Availability

We wholeheartedly agree with you on the importance of open source. We will release all the data and code of this paper (pending compliance review), including the test datasets, the implementation of LIPS and MCTs, as well as our Lean and SMT formalizations.

2. Possibility of Unintended Errors When Formalizing Math Problems

Our problem domain is immune to many formalization errors plaguing existing benchmarks such as MiniF2F [1]. A common source of errors arises from issues with natural numbers or integers in Lean 4, e.g., algebra_ineq_nto1onlt2m1on. The inequalities proved by LIPS are not affected by such errors because they only involve real variables, without integers or natural numbers. Furthermore, we have manually checked the formalization of inequalities in our test datasets and plan to release them upon publication.

[1] Zheng, Kunhao, Jesse Michael Han, and Stanislas Polu. "Minif2f: a cross-system benchmark for formal olympiad-level mathematics." arXiv 2021

3. Algorithm for Proof Search

We used best-first search, with LLMs for ranking the open proof goals in each iteration (Sec. 4.2). We will revise the paper to describe the proof search algorithm explicitly and in more detail. Thank you for the suggestions!

4. Missing Related Works

Thank you for suggesting relevant papers we have missed. We have included them in the revision.

5. Using Simpler ML Models Instead of LLMs

In principle, it is possible to replace LLMs in LIPS with simpler models. However, we would have to solve two challenges: First, the model must generate effective rewriting tactics from an infinite space of possible rewrites. Second, it must learn from limited data. Pre-LLM models typically struggle with open-ended generation and zero-shot prediction. Therefore, using them in LIPS may require significant redesign of the method.

6. Time Limit vs. Proof Success Rate

For LIPS, We present the proving success rates under different time limits in the table below. The results indicate that the success rate of LIPS improves gradually as more time is allocated. Although symbolic solvers (CAD and MMA) verify the inequalities in under 10 minutes, it is important to note that symbolic solvers are unable to construct human-readable proofs for the problems. Additionally, we plan to further enhance the efficiency of LIPS in future versions, for example, by optimizing the SymPy pattern_matching function.

7. Selecting Lemmas and the Filtered Size Hyperparameter

The lemmas used in LIPS' scaling tactics, detailed in Appendix C (LIPS paragraph), were constructed from [1, 2, 3] and are all standard inequalities (e.g., Cauchy-Schwarz, Chebyshev, and Hölder) commonly used by human contestants in math competitions. None of the lemmas is tied to any particular problem in the test set.

The size of the filtered set is primarily influenced by the LLM's ability to accurately identify a promising proof candidate. In practice, determining the optimal size using a validation set can be computationally expensive. In our experiment, we adopt the ``needle in a haystack’’ approach. Starting with an inequality (e.g., $ab+bc+ca \leq a^2 + b^2 + c^2$) as the initial seed, we manually generated a series of proof candidates. The size of the proof candidates was incrementally increased until the LLM could no longer reliably select the best candidate.

[1] Mildorf, Thomas J. "Olympiad Inequalities." Preprint, https://artofproblemsolving.com/articles/files/MildorfInequalities.pdf

[2] Wei, Chenrui, Mengzhou Sun, and Wei Wang. "Proving Olympiad Algebraic Inequalities without Human Demonstrations." NeurIPS Datasets and Benchmarks Track 2024

[3] Kozma, L. Useful Inequalities. Preprint, https://www.lkozma.net/inequalities_cheat_sheet/ineq.pdf

8. Potential Data Contamination Due to the Use of GPT-4o

Please see our common response at the top of this page.

9. Ablations of Symbolic Filtering, Sum-of-squares and Tangent Line

Please see additional ablations in the common response at the top of this page.

10. Minor Errors and Writing Suggestions

Thank you for your detailed comments. We will incorporate them into the next revision, adding more introduction to theorem proving in Lean, fixing Figure 3 and 4, as well as spelling out the full names of acronyms such as AM-GM inequality.

(Connect to Part 2)

Response to Additional Questions

Thank you for your detailed questions. We address them individually.

Q1: Could you provide the Lean and SMT formalizations of the test inequalities?

Q2: Could you provide the implementation of LIPS?

Yes, we plan to open source the data and code of this paper.

Q3: What precise parameters were used for SMT solvers to obtain the CAD baseline?

For z3, we use default parameters. For cvc5, we use default parameters except that nl-cov-force is set to True for enabling CAD.

Q4: How is MCTS implemented? Do you apply symbolic filtering during the search, similarly as in LIPS?

Our MCTS implementation follows the approach introduced in AIPS [1], with details described in Appendix C. Symbolic filtering is not used during MCTS.

[1] Wei et al. "Proving Olympiad Algebraic Inequalities without Human Demonstrations." NeurIPS Datasets and Benchmarks Track 2024

Q5: Why do you write "Please reason step by step" in the prompts for neural ranking? What are the full resulting responses from GPT-4o?

Instructing LLMs to reason step by step was introduced by Kojima et al. [1] and is widely used for eliciting chain-of-thought in LLM’s response without providing explicit chain-of-thought examples in the prompt.

For the input prompt in Sec. 4.2, GPT-4o’s output is:

To rank the transformations in terms of their ability to reduce the proving difficulty, we need to evaluate each transformation step by step.

### Original Inequality
The original inequality is:

$

\frac{1}{a^2+2} + \frac{1}{b^2+2} + \frac{1}{c^2+2} \leq \frac{1}{3a^2+3b^2+c^2} + \frac{1}{3b^2+3c^2+a^2} + \frac{1}{3a^2+3c^2+b^2}

$

with the condition $a^2 + b^2 + c^2 = 1$.

### Transformations

#### Transformation (1)

$

\frac{1}{a^2 + 2} + \frac{1}{b^2 + 2} + \frac{1}{c^2 + 2} \leq 2 \sqrt{\frac{1}{a^2 + 3b^2 + 3c^2} \cdot \frac{1}{b^2 + 3a^2 + 3c^2}} + \frac{1}{c^2 + 3a^2 + 3b^2}

$

- This transformation involves using the AM-GM inequality to combine terms, which simplifies the comparison of left and right sides.
- It leverages symmetry and reduces the complexity slightly by introducing a square root, which can be easier to handle in some contexts.

#### Transformation (2)

$

\frac{1}{a^2 + 2} + \frac{1}{b^2 + 2} + \frac{1}{c^2 + 2} \leq \frac{9}{7a^2 + 7b^2 + 7c^2}

$

- This transformation simplifies the problem by reducing the right-hand side to a single fraction.
- It takes advantage of the condition $a^2 + b^2 + c^2 = 1$, simplifying the denominator on the right-hand side to a constant value $7$.

#### Transformation (3)

$

\frac{1}{a^2 + 2} + \frac{1}{b^2 + 2} + \frac{1}{c^2 + 2} \leq \frac{1}{3 - 2a^2} + \frac{1}{3 - 2b^2} + \frac{1}{3 - 2c^2}

$

- This transformation attempts to reframe the right-hand side using $3 - 2a^2$, $3 - 2b^2$, and $3 - 2c^2$.
- The symmetry of this transformation is useful, but it does not significantly simplify the structure of the inequality.

### Ranking
1. **Transformation (2)** is the most meaningful because it reduces the entire right side to a constant dependent only on the given condition, which significantly simplifies proving the inequality.
2. **Transformation (1)** is also a meaningful transformation, as it uses AM-GM inequality to introduce a symmetric form that could be easier to manage.
3. **Transformation (3)** is the least meaningful in terms of simplifying the proving process, as it does not reduce the complexity as effectively as the others.

Thus, the ranking in descending order of transformation effectiveness is:

$

\boxed{\{(2), (1), (3)\}}

$

[1] Kojima, Takeshi, et al. “Large language models are zero-shot reasoners.” NeurIPS 2022

Q6: 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?

During best-first search, each iteration involves using the tactic generator to expand the most promising proof goal. Consequently, “Iteration of LIPS” refers to the number of times the tactic generator is invoked. “Iteration” in the oracle means the number of tactics in the final proof. Thank you for pointing out the confusion. We will clarify these terms in the next revision.

Q7: How does search work in LIPS? Is it best-first search? Or breadth-first search?

Best-first search, as addressed in a previous remark.

Q8: 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?

In Figure 3, the X-axis represents the indices of all problems successfully proved by LIPS, totaling 16 problems. As illustrated in Figure 3(a), LIPS underperforms the existing method on only three problems (indexed as 10, 15, and 16). Thus, we conclude that LIPS outperforms the existing method on at least 13 problems. We will clarify it in the revision.

(Connect to Part 3)

Now I also think that more fair comparison to CAD/SMT-based methods would involve appending the pre-designed 96 scaling tactics and 16 rewriting tactics to the input inequality problems provided to the SMT solvers. Could you comment on that? Perhaps the lower CAD performance is because the SMT solvers did not have the access to the prior knowledge encoded in the pre-designed tactics?

Also, I agree with you that the symbolic methods you test are not outputting interpretable proofs, but it does not mean that they cannot be made interpretable/readable. Perhaps you could also rewrite/reconstruct the SMT proofs into Lean proofs.

./cvc5 cvc5_formalizations/1.smt
cvc5_formalizations/1.smt:1.2: No set-logic command was given before this point.
cvc5_formalizations/1.smt:1.2: cvc5 will make all theories available.
cvc5_formalizations/1.smt:1.2: Consider setting a stricter logic for (likely) better performance.
cvc5_formalizations/1.smt:1.2: To suppress this warning in the future use (set-logic ALL).
(error "Parse Error: cvc5_formalizations/1.smt:7.22: expecting same arithmetic types to POW")

1. Broad Impact and Generality of LIPS (4dY9, cEd1, v6PZ, YrrG)

While LIPS focuses on a concrete domain—inequality problems in pre-college math competitions (described in Figure 1)—it makes important contributions and can potentially generalize to other domains. First, the inequality problems tackled by LIPS are important beyond competition-level mathematics. They are closely related to quantifier-free non-linear real arithmetic (QF_NRA) in SMT (Satisfiability Modulo Theories), which plays a foundational role in formal verification [1]. One potential application of LIPS is to enhance SMT solvers by serving as a QF_NRA backend.

Furthermore, inequalities are pervasive not only in pre-college math competitions but also in many branches of advanced mathematics, including analysis, statistics, and information theory. For example, a recent breakthrough in partial differential equations (PDEs)—the proof of blowup for the Euler equations [2]—relied heavily on inequalities. As highlighted by a Quanta Magazine article [3], "Hou and Chen had to prove the statement, which boiled down to a complicated inequality involving terms from both the re-scaled equations and the approximate solution." Although the inequalities encountered in advanced mathematics often extend beyond the current capabilities of LIPS (e.g., involving calculus), they share many foundational techniques, such as rewriting and scaling, which are utilized by LIPS. Extending LIPS to handle inequalities in other mathematical domains is a promising direction for future work. To demonstrate the feasibility, we use LIPS to prove the negativity of the KL divergence between two binomial distributions—an important result in information theory. LIPS is able to generate the following proof, which cancels out a nonnegative factor $n$, rearrange the inequality, and apply the Jensen inequality.

theorem KL_nonnegativity {n a b : ℝ} (ha : a > 0) (ha' : 1 - a > 0) (hb : b > 0) (hb' : 1 - b > 0) (hn : n > 0) : 0 ≤ n * a * log (a / b) + n * (1 - a) * log ((1 - a) / (1 - b)) := by
 llm_cancel_factor 0 - (n * a * log (a / b) + n * (1 - a) * log ((1 - a) / (1 - b))) = (-n)*(a*log (a/b) + (1-a)*log ((1-a)/(1-b)))
 llm_simplify 0 - (a * log (a / b) + (1 - a) * log ((1 - a) / (1 - b))) = a * log (b/a) + (1 - a) * log ((1-b)/(1-a))
 scale NEQ_weighted_Jensen_logx_left (i1 := a) (i2 := (1-a)) (u := (b/a)) (v := ((1-b)/(1-a))) (right := 0)
 llm_simplify (a + (1 - a)) * log ((a * (b / a) + (1 - a) * ((1 - b) / (1 - a))) / (a + (1 - a))) = 0

Abstracting away from specific system designs, the principles underlying LIPS are highly general and transferable to other domains. A primary challenge in mathematical theorem proving, unlike board games such as Go, is the infinite action space [4], which resists effective exploration. A key insight of LIPS is that domain knowledge can enable the design of an action space that allows symbolic reasoning to efficiently explore at least a subset of the space. This general principle has been successfully applied in other domains. For instance, AlphaGeometry [5] partitions its action space into two categories: deducing properties from the premises of an existing geometry problem and introducing auxiliary constructions (e.g., points, lines, or circles). The former category is particularly amenable to symbolic reasoning, analogous to the scaling tactics in LIPS.

The reviewers' question on generality is insightful and related to a central debate in AI for Mathematics: Should we strive to build generalist AI systems that are agnostic to mathematical domains, or should we develop specialist systems tailored to specific domains? This dichotomy is reflected in recent works—generalist approaches such as LeanDojo [6] and specialist approaches such as AlphaGeometry, FunSearch [7], and LIPS. Mathematics has an infinite action space. To effectively explore it, we must leverage its structure. The generalist approach assumes that AI can learn and exploit domain-specific structures and idiosyncrasies in a general way. While this approach is desirable in the long term, it faces challenges with the current generation of technology. In contrast, specialists rely on human-designed structures informed by mathematical knowledge, e.g., scaling and rewriting tactics in LIPS. This approach is more practical and effective in the short to medium term. Therefore, we believe AI math specialists like LIPS have value and will coexist with generalists for the foreseeable future.

(Connect to Part 3)

2. Additional Ablations (4dY9, cEd1)

Thank you for suggesting these ablations. We will incorporate the results into the next revision.

• Scaling Tactics: Figure 4 (a) has shown how the performance on the ChenNEQ dataset (Y axis) changes as we increase the number of lemmas used by scaling tactics (X axis). When X = 0 (without scaling tactics), only 3 out of 41 theorems can be proved, whereas LIPS can prove 39 theorems.
• 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). A smaller X 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 X beyond 32, as this consistently caused GPT-4o to hit the maximum token limit (set at 4096)
• Sum-of-squares and Tangent Line Tricks: We newly evaluated LIPS w/o sum-of-squares and tangent lines on ChenNEQ. Among the 39 out of 41 proved inequalities, only 1 requires sum-of-squares, and 3 requires the tangent line trick.
• Neural Ranking: Figure 5 presents an ablation analysis where neural ranking is replaced with random selection. The results demonstrate a significant drop in LIPS performance, from 95.1% to 41.2%, underscoring the necessity of neural ranking. Additionally, we plan to incorporate a new ablation analysis that examines the effect of replacing neural ranking with purely symbolic filtering.

3. Potential Data Contamination Due to GPT-4o (cEd1, v6PZ)

We agree with the reviewers on the importance of vigilance against data contamination when evaluating LLM-based methods. However, our analysis indicates that data contamination is unlikely to be a significant contributor to LIPS’s performance.

In Sec. 5.2 (RQ1), we asked OpenAI o1 to prove the 20 problems from the MO-INT dataset and manually evaluated the generated proofs. o1 wasn’t able to prove any one of them. We repeated this experiment using GPT-4o, and the results were the same, indicating that LLMs did not memorize the proofs of test problems during pretraining. In addition, even if they had memorized the (human-written) proofs, it is difficult to translate them from English/LaTex into a formal language like Lean, i.e., autoformalization.

4. Implementation Details of Rewriting Tactics in Lean 4 (cEd1, v6PZ)

We implemented LLM-generated rewriting using 16 Lean 4 tactics. For the complete list, please refer to Appendix C (LIPS paragraph). We will release all the data and code of this paper (pending compliance review), including the Lean 4 implementation of these tactics.

The neural rewriting essentially attempts to transform the current inequality into an equivalent form, which is generated by LLMs. The rewriting tactic in Lean 4 then only needs to verify whether this new form is provable. For instance, given the original inequality $ab+bc+ca \leq a^2+b^2+c^2$, the LLM might produce a new version like $3ab+3bc+3ca \leq (a+b+c)^2$. The rewriting tactic is then invoked to check whether the transformation $(ab+bc+ca) - (a^2+b^2+c^2) = (3ab+3bc+3ca) - (a+b+c)^2$ holds.

To achieve this, we integrate a series of Lean 4 automation tactics under the llm_simplify function:

macro "llm_simplify " h:term : tactic =>
    `(tactic| (apply move_left;
                rwp [show $h by
                (first
                | ·field_simp [*]
                | ·(field_simp; ring)
                | ·(field_simp [*]; ring)
                (try simp only [tsub_le_iff_right]);
                (try apply tsub_le_iff_right_p);
                norm
              ))

Other rewriting tactics follow a similar structure.

[1] De Moura, Leonardo, and Nikolaj Bjørner. "Satisfiability modulo theories: introduction and applications." CACM 2011

[2] Chen, Jiajie, and Thomas Y. Hou. "Stable nearly self-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data I: Analysis." arXiv 2022

[3] Jordana Cepelewicz. "Computer Proof ‘Blows Up’ Centuries-Old Fluid Equations." Quanta Magazine 2022

[4] Poesia, Gabriel, and Noah D. Goodman. "Peano: learning formal mathematical reasoning." Transactions of the Royal Society A 2023

[5] Trinh, Trieu H., et al. "Solving olympiad geometry without human demonstrations." Nature 2024

[6] Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." NeurIPS 2024

[7] Romera-Paredes, Bernardino, et al. "Mathematical discoveries from program search with large language models." Nature 2024