Proving Olympiad Algebraic Inequalities without Human Demonstrations

Authors: chenrui  wei
wei  wang
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-19 14:38:49

Abstract: Solving Olympiad-level mathematical problems represents a significant advancement in machine intelligence and automated reasoning. Current machine learning methods, however, struggle to solve Olympiad-level problems beyond Euclidean plane geometry due to a lack of large-scale, high-quality datasets. The challenge is even greater in algebraic systems, which involve infinite reasoning spaces within finite conditions. To address these issues, we propose *AIPS*, an *Algebraic Inequality Proving System* capable of autonomously generating complex inequality theorems and effectively solving Olympiad-level inequality problems without requiring human demonstrations. During proof search in a mixed reasoning manner, a value curriculum learning strategy on generated datasets is implemented to improve proving performance, demonstrating strong mathematical intuitions. 
On a test set of 20 International Mathematical Olympiad-level inequality problems, AIPS successfully solved 10, outperforming state-of-the-art methods. Furthermore, AIPS automatically generated a vast array of non-trivial theorems without human intervention, some of which have been evaluated by professional contestants and deemed to reach the level of the International Mathematical Olympiad. Notably, one theorem was selected as a competition problem in a major's city 2024 Mathematical Olympiad.

Main paper: 
 introduction: 
 One of the key milestones in the field of artificial intelligence is the capability to reason (Pearl 1998) and prove theorems (Wu 1978; Chou et al. 2000; Trinh et al. 2024 ). However, theorem proving often involves long reasoning chains, complex mathematical structures, intricate calculations, and infinite reasoning spaces. Consequently, developing AI capable of proving complex mathematical theorems requires sophisticated reasoning and the ability to navigate through an extensive search space to construct a valid proof. The complexity of these problems lies in the need for effective heuristics and strategies to manage the vast number of possible actions and the lengthy sequences of logical steps necessary to arrive at a solution.Existing work on grade school and college admission math problems has achieved remarkable success, e.g., GSM8K (Cobbe et al. 2021 ) and SAT Math (Achiam et al. 2023) . However, research focusd on solving International Mathematical Olympiad (IMO)-level problems remains relatively sparse. Notable efforts in this area include AlphaGeometry (Trinh et al. 2024) , and GPT-f (Polu and Sutskever 2020) on miniF2F (Zheng et al. 2021) , which have made progress in solving Euclidean plane geometry at the Olympiad level and various mathematical competition problems, respectively.A significant challenge for learning-based methods in this domain is the scarcity of suitable datasets, which limits the ability to train models effectively and hampers progress in achieving human-level performance on these hard problems. AlphaGeometry (Trinh et al. 2024) addresses this issue by synthesizing millions of theorems and proofs across different levels of complexity to train a neural language model from scratch. Similarly, the INequality Theorem proving benchmark, INT (Wu et al. 2020) , can synthesize a theoretically unlimited number of theorems and proofs in the domain of algebraic equalities and inequalities. However, INT focuses on testing a learning-assisted theorem proving agent's generalization ability rather than increasing the difficulty to competition level. Another significant challenge in automated theorem proving is designing effective search strategies to navigate the vast space of possible proofs. Recent advancements have highlighted various approaches to enhance search efficiency and proof success rates. Some studies have shown that incorporating Monte Carlo Tree Search (MCTS) can significantly aid in proving new theorems (Wu et al. 2020) . Inspired by the success of AlphaZero (Zhang and Yu 2020) , other research has explored HyperTree Proof Search (HTPS) (Lample et al.) , which learns from previous proof searches through online training, iteratively improving its strategy by learning which paths are more likely to lead to successful proofs. Another innovative approach starts the proof search from the root goal that needs to be proved (Polu and Sutskever 2020) , expanding a maintained proof tree by prioritizing open goals based on their cumulative log probability.In this work, we introduce AIPS, an Algebraic Inequality Proving System, which can generate a large number of high-quality theorems and solve IMO-level algebraic problems. AIPS focuses on ternary and quaternary inequalities, excluding n-variable inequalities represented recursively in formal verification systems. Among the generated theorems, some have proven to be very challenging, with one selected for a major city's 2024 Mathematical Olympiad. We present novel and challenging inequality theorems discovered by AIPS in the supplementary material, which have been carefully evaluated by IMO-level professional contestants and found to be comparable to IMO inequalities from around the year 2000.Additionally, AIPS incorporates a value network to evaluate newly generated inequalities, selecting subgoal candidates based on the top scores provided by the value network. The value network is trained on synthetic datasets with increasing difficulty in a curriculum manner. In our experiments, AIPS proved difficult theorems up to the IMO level and solve 10 out of 20 problems in an IMO-level inequality test, significantly surpassing the performance of previous Large Language Model-based theorem provers (Polu and Sutskever 2020; Polu et al. 2022; Yang et al. 2024; Song et al. 2024) .The main contributions in this paper are summarized as follows:• We propose a symbolic deductive engine capable of efficiently generating high-quality and solving high-difficulty algebraic inequality theorems. This engine addresses the bottleneck of lacking large-scale, high-quality data in this field.• We demonstrate that a symbolic algebraic inequality prover can be significantly enhanced under the guidance of a value network, especially when the value network is trained in a curriculum manner.• Our AIPS can generate challenging and elegant inequality theorems, with one theorem selected for a major city's Mathematical Olympiad. AIPS can prove 10 out of 20 IMO-level inequalities, outperforming state-of-the-art methods.2 Algebraic Inequality Proving System 
symbolic deductive engine for algebra: 
 Interactive theorem provers, such as Lean, can verify mathematical operations but lack the ability to perform automatic mathematical reasoning by combining computational rules. This challenge is amplified in the automatic proof of algebraic inequalities, which often involves numerous calculations, extensive transformation rules, and complex theorem matching. To address this, we designed a symbolic deductive engine that integrates with SymPy1 , supporting algebraic reasoning through theorem matching and applying transformation rules. Please refer to Appendix A for more details.One of the main challenges in enabling learning-based models to solve complex mathematical problems is the scarcity of large-scale, high-quality datasets. To overcome this obstacle, we develop a theorem generator that effectively generates Olympiad-level inequality theorems by implementing a forward reasoning method.We selected 10 synthetic problems and invited Olympiad medalists to evaluate their difficulty and elegance. Some generated theorems exceeded the difficulty of early IMO inequalities, with one theorem being used in a city's 2024 Mathematical Olympiad. Evaluation details are provided in Appendix C.Figure 1 : Example of generating synthetic theorems in AIPS.By leveraging the capabilities of the deductive engine and the Best-First-search algorithm (Dechter and Pearl 1985) , we train an inequality prover through value curriculum learning. This prover formulates the algebraic inequality proving as a sequential decision-making process by selecting theorems to generate highly human-readable proofs. As shown in Fig. 2 , given a goal and related conditions, AIPS first generates a list of subgoals by applying a set of theorems at each iteration. A value neural network is then used to evaluate these newly generated subgoals along with the previous subgoals. The top-value subgoal is selected for the next step of reasoning. This iterative process continues until the proof is successfully completed. See Appendix A.5 for more details.The rating scores by the three professional contestants are reported in Table 2 . The third expert does not assign scores to the four IMO problems, believing the average difficulty of the ten problems is significantly lower than that of IMO problems. The first expert does not give a difficulty score for Problem 8 because he does not solve it. From the table, we observe that while the average difficulty does not compare with IMO inequalities, a few problems, such as Problem 9 and Problem 7, reach the IMO level. Among the 10 synthetic problems above, problem 4 was chosen as a competition problem in a major city's 2024 Mathematical Olympiad, as shown in Fig. 13 . It received positive feedback for its appropriate difficulty, concise form, and variety of solutions. This problem was posted online, and 75 contestants provided their evaluations on its difficulty and elegance. The score distributions are shown in Fig. 14 . The average difficulty score was 3.3 out of 7, and the elegance score was 2.2 out of 5. The 4 solutions to this problem, including one provided by our AIPS and 3 solutions collected from the competition organizers, are given as follows.Problem: Given three positive real numbers a, b, c, prove that2a √ 2a 2 + b 2 + c 2 + 2b √ 2b 2 + c 2 + a 2 + 2c √ 2c 2 + a 2 + b 2 ≤ 3 √ 2(a + b + c) √5a 2 + 5b 2 + 5c 2 + ab + bc + ca ≥ 2a √ 2a 2 + b 2 + c 2 (2)Where denotes cyclic summation. The proof of (1) follows from the fact that a 2 +b 2 +c 2 ≥ ab + bc + ca. For the second part, we apply Chebyshev's inequality. Without loss of generality, we assume a ≥ b ≥ c. First notice that which is equivalent to 3a 2 t 4 S + 3a 2 t 2 S 2 ≤ (2Sa 3 t 3 + St 6 ) + (2S 2 ta 3 + S 2 a 4 )The last inequality is proved by applying AM-GM inequality. 
experiments: 
 We evaluate AIPS as well as 10 different baseline models on MO-INT-20, an Olympiad-level inequality problem test set, with each problem limited to 90 minutes of solving time, consistent with the standard problem-solving time in the IMO. It outperforms the state-of-the-art methods in terms of the number of solved problems, demonstrating the strong algebraic intuitions developed by the learned value network. The comparison results are shown in Table 1 .Analysis. Large language models (LLMs), formal theorem provers, and neural symbolic provers each demonstrate distinct strengths in the test. LLMs often make trivial logical or computational errors. Formal theorem provers, such as LeanCopilot, struggle with planning the proof for complex math problems. Neural provers with different search method and heuristics show different performance in the test. Please refer to Appendix B.5 for more details. Following a curriculum learning strategy on 1,000 inequality problems, AIPS achieves the best performance, solving 10 out of 20 problems. Among the 10 problems from the IMO or IMO shortlist, it successfully solves five, reaching the average level of IMO contestants. We also test the performances of AIPS after 200, 400, 600, and 800 loops of fine-tuning value network (see Appendix B.3). The results demonstrate that our value curriculum learning strategy is very effective, with the number of proof search steps significantly decreasing during the training process, and the number of solved problems increasing to 10 ultimately.By <function try_homo>, it is equivalent to provea 2 b 2 c(a + b) + b 2 c 2 a(b + c) + a 2 c 2 b(a + c) ≥ 3a 2 3 b 2 3 c 2 3 2We use Hölder's inequality:ab + bc + ca 2 ≤ (c(a + b) + a(b + c) + b(c + a))( a 2 b 2 c(a + b) + b 2 c 2 a(b + c) + a 2 c 2 b(a + c)). To prove 
conclusion: 
 In conclusion, solving Olympiad-level mathematical problems is a significant milestone in machine intelligence and automated reasoning. The lack of large-scale, high-quality datasets presents a challenge, particularly in algebraic systems. To address this, we propose AIPS, an Algebraic Inequality Proving System, which autonomously generates complex inequality theorems and effectively solves Olympiad-level inequality problems without human input. Utilizing a value curriculum learning strategy, AIPS demonstrated strong mathematical intuition by solving 10 out of 20 International Mathematical Olympiad-level problems. One of these theorems was selected for a major city's 2024 Mathematical Olympiad. 
solution to polish-2004 problem: 
 We use Hölder's inequality: by <function try_expand_r>, it remains to proveEQUATION0 ≤ 4a 3 b + 4a 3 c + 4a 3 d + 6a 2 b 2 + 12a 2 bc + 12a 2 bd + 6a 2 c 2 + 12a 2 cd + 6a 2 d 2 + 4ab 3 . . .by <function check_AM_GM>, it remains to prove By <function try_homo>, it is equivalent to prove0 ≤ 4a 3 b + 4a 3 c + 4a 3 d + 6a 2 b 2 + 12a 2 bc + 12a 2 bd + 12a 2 cd + 6a 2 d 2 + 4ab 3 . . .a 3 b 3 c 2 (a + 2b) 2 + a 3 c 3 b 2 (2a + c) 2 + b 3 c 3 a 2 (b + 2c) 2 ≥ a 2 3 b 2 3 c 2 33 we use Hölder's inequality:(ab + ac + bc) 3 ≤ (a(b + 2c) + b(2a + c) + c(a + 2b)) 2 × (a 3 b 3 /(c 2 (a + 2b) 2 ) + a 3 c 3 /(b 2 (2a + c) 2 ) + b 3 c 3 /(a 2 (b + 2c) 2 )). It remains to prove a 2 3 b 2 3 c 2 3 3 ≤ ab 9 + ac 9 + bc 9 by <function check_AM_GM>, this is true! 9. Solution to Korea-2011-P4. To prove 1 a 2 -4a + 9 + 1 b 2 -4b + 9 + 1 c 2 -4c + 9 ≤ 7 18 , we have f (x) = 1/(x 2 -4x + 9) ≤ 2 + x 18 for 0 < x < 1 ⇐⇒ - x (x -1) 2 18 (x 2 -4x + 9) ≤ 0 for 0 < x < 1, which is true. Substitute x for a/(a + b + c), we have 1/(a 2 -4a + 9) = (a + b + c) 2 a 2 -4a (a + b + c) + 9 (a + b + c) 2 ≤ 3a + 2b + 2c 18a + 18b + 18c.It remains to prove3a + 2b + 2c 18a + 18b + 18c + 2a + 3b + 2c 18a + 18b + 18c + 2a + 2b + 3c 18a + 18b + 18c ≤ 7 18 ,by <function try_together_l>, this is true. 
solution to japan-2014-p5: 
 By <function try_homo>, it is equivalent to provea (a + b + c) 9bc + 4 (b -c) 2 + (a + b + c) 2 + b (a + b + c) 9ac + 4 (-a + c) 2 + (a + b + c) 2 + c (a + b + c) 9ab + 4 (a -b) 2 + (a + b + c) 2 ≥ 1 2 .We use Hölder's inequality:(a + b + c) 3 ≤ ( a (a + b + c) 9bc + 4 (b -c) 2 + (a + b + c) 2 + b (a + b + c) 9ac + 4 (-a + c) 2 + (a + b + c) 2 + c (a + b + c) 9ab + 4 (a -b) 2 + (a + b + c) 2 )× a 9a 2 + 4 (b -c) 2 + (a + b + c) 2 + b 9b 2 + 4 (-a + c) 2 + (a + b + c) 2 + c 9c 2 + 4 (a -b) 2 + (a + b + c) 2 It remains to prove 1 2 ≤ (a + b + c) 3 27abc + 4a (b -c) 2 + a (a + b + c) 2 + 4b (a -c) 2 + b (a + b + c) 2 + 4c (a -b) 2 + c (a + b + c) 2by <function nodiv_expr>, it remains to prove27abc + 4a (b -c) 2 + a (a + b + c) 2 + 4b (a -c) 2 + b (a + b + c) 2 + 4c (a -b) 2 + c (a + b + c) 2 ≤ 2 (a + b + c) 3 by <function zero_side>, it remains to prove 0 ≤ -27abc -4a (b -c) 2 -a (a + b + c) 2 -4b (a -c) 2 -b (a + b + c) 2 -4c (a -b) 2 -c (a + b + c) 2 + 2 (a + b + c) 3 by <function try_expand_r>, it remains to prove 0 ≤ a 3 -a 2 b -a 2 c -ab 2 + 3abc -ac 2 + b 3 -b 2 c -bc 2 + c 3 by <function check_schur>, this is true! 
 
 Appendix: We provide more information on AIPS' deductive engine and the training process for the value network. To highlight the reasoning ability and maintain readability of proofs, we avoid using brute-force methods such as augmentation-substitution and Wu's method Wu (1978) .Theorem proving encompasses two types of reasoning: forward reasoning and backward reasoning. Forward reasoning involves identifying a pattern match between a particular theorem and the given conditions along with the universal variables, then deducing the conclusion. In contrast, backward reasoning works in the opposite direction, where the conclusion and variables are matched with a specific theorem, breaking down the main goal into smaller, more manageable subgoals. Both methods are essential in constructing and navigating the logical steps to establish the validity of complex mathematical theorems, as shown in Fig. 3 . There are two main challenges in reasoning within algebraic systems. The first is the infinite reasoning space within finite conditions, caused by the numerous possible expression trees and the vast search space for premises. This contrasts with solving Euclidean geometry problems, where a deduction fixed point exists with respect to a set of geometric rules or axioms. To address this issue, we consider only the current expression tree at each step of reasoning. The second challenge lies in pattern matching, which requires accurately identifying and applying relevant theorems to given sub-structures. For theorems with function-type variables, like Jensen's Inequality, pattern matching is more challenging and time-consuming. We provide heuristic functions to identify possible structures where Jensen's Inequality can be applied.Algebraic expressions are represented symbolically with an underlying expression tree structure in AIPS as shown in Fig. 4 . Our system matches theorems to algebraic expressions by traversing the expression tree and updating node labels based on how the expression changes. If a match is found, the sub-expression is replaced, generating a new inequality. Our deductive engine incorporates six well-known inequality theorems frequently used in mathematical Olympiads, several one-variable inequality scaling and solving methods, and dozens of algebraic transformation rules. The inequality theorems include the Arithmetic Mean-Geometric Mean (AM-GM) inequality, the weighted AM-GM inequality, Hölder's inequality, Jensen's inequality, Schur's inequality, and Müirhead's theorem. For simplicity, we have excluded some theorems that can be directly proved using these inequalities, such as the Geometric Mean-Harmonic Mean (GM-HM) inequality and the Cauchy-Schwarz inequality.Here we list some frequently used methods and transformation rules: • all_cyc_mul_expr: Multiply both sides by a cyclically symmetric polynomial, with one of its generators on either the left or right side of the inequality (a generator is a term that, when cyclically permuted, generates the expression)• try_factor_both: Factorize both sides• check_one_var: Check if the solution of a one-variable inequality is contained in a given interval• check_linear_ctr: Check if a one-variable expression can be applied with tangent line trick• find_main_fun: For a cyclically symmetric expression, try to find a function that can match with Jensen's inequality as well as generate this expressionAn important step in generating synthetic theorems is matching algebraic expressions with these theorems. We use the AM-GM inequality as an example to illustrate pattern matching method as follows.Theorem 1. (AM-GM) For non-negative real numbers a 1 , a 2 , . . . , a n ,a 1 + a 2 + • • • + a n ≥ n n √ a 1 a 2 • • • a n with equality if and only if a 1 = a 2 = • • • = a n .Assuming all variables are non-negative, pattern matching for an algebraic expression with the AM-GM inequality (on the Left-Hand-Side) is explained in three steps:1. Traverse through the expression tree, and label a node with 1 if the whole expression value increases as the value of the node increases, with -1 if the expression value decreases as the value of the node increases, and with None if this cannot be determined. 2. At each node labeled 1 or -1 and calculated with an Add operation, find all non-negative sub-arguments of the node's expression and place them in nonneg_set. Similarly, find all non-positive sub-arguments and place them in nonpos_set. 3. For the obtained sets nonneg_set and nonpos_set, we use the following method to match the mean inequalities:• Arbitrarily partition each set into multiple subsets.• the sum of the elements in each subset can be used as a variable to match the left side of the mean inequality. • If a subset does not contribute to the inequality, it is excluded from the partition. This process allows us to identify all possible mean inequalities that can be matched. We then replace the original sub-expressions in the expression tree with the transformed ones based on the matched inequalities. By doing so, a new inequality is derived according to the labels.Olympiad inequalities aim for not only difficulty but also conciseness and elegance, a principle also valued in modern mathematics. Although our deductive engine can generate various types of inequalities, we focus on cyclically symmetric inequalities in semi-definite systems that can be generated with a limited number of steps to avoid lengthy and chaotic expressions.Initially, we generate thousands of premises as the starting points for data generation using Algorithm 2. For each generated premise, we run the data-generation algorithm 1. Fig. 1 shows the generation process. During this process, we discard inequalities for which equality does not hold or which do not have the desired form, and halt the generation after a maximum of 25 iterations of search. Utilizing 32 CPUs over an 8-hour period, the deductive engine produces 191,643 theorems. This demonstrates the engine's ability to efficiently generate a large number of high-quality inequality theorems, thereby addressing the bottleneck of lacking a high-quality dataset for learning-based provers.Algorithm 1 Generating Theorems 1: function Generate_Theorems(expression P , loops N ) 2: Initialize Theorem Set S, Transformation Rules O, Inequality Sets A1, A2, A3 3: Apply S to P to generate inequalities and add those with equality conditions to R 4: for i ← 1 to N do 5:for each inequality ineq in R do for each inequality ineq in R do In this section we describe the neural network for value curriculum learning, its training process and how it is utilized for guiding proof search.The procedure of searching for inequality proofs is generally divided into three parts: mixed reasoning for subgoal generation, evaluation, and planning.Subgoal Generation. There are two methods for generating subgoals in AIPS. The first method involves applying fundamental inequality theorems. Let X be the set of variables. Suppose the inequality theorem to prove is u(X) ≤ v(X) under a condition set P. AIPS first homogenizes the inequality to f (X) ≤ g(X) on both sides by applying conditions in P. Then, by applying theorems to the left-hand side of the target inequality, AIPS generates a series of new inequalities:f (X) ≤ h 1 (X), . . . , f (X) ≤ h n (X)This results in subgoals h i (X) ≤ g(X). Similarly, by applying theorems to the right-hand side, AIPS also generates subgoals f (X) ≤ s j (X). The second method involves applying transformation rules such as sympy.expand and sympy.apart to the goal, generating subgoals that are equivalent to the original inequality.Evaluation. AIPS employs a value function V θ to assess the difficulty of each inequality. Formally, we have a function f parameterized by η that encodes the inequality expression s. The encoded embedding vector f η (s) is then fed into a deep neural network g ϕ , which outputs a value in the interval [0,1]. We choose f to be a transformer encoder with average pooling (Vaswani et al. 2017) .Planning. With the evaluation function V θ , we use the Best-First search algorithm for planning. We also test the performance of Monte-Carlo Tree Search (MCTS) algorithm, where the result is less satisfactory. There are two primary reasons for this. First, the action space for each state is extremely large, leading to explosive growth of the MCTS searching tree. Second, the high cost of reasoning steps makes the simulation step in MCTS nearly impractical, often exceeding time limits.We also note that our prover can be combined with any heuristic function, and thus design various baselines in our experiments.We define the tree-depth D of an inequality as the maximum depth of the expression trees on both sides. Proving an algebraic inequality is equivalent to reducing the tree-depth of the inequality to one. We use D as the supervision information to train initial heuristic function f init in the Best-First search algorithm. That is to say, we pre-train a value network V θ as f init on the synthetic dataset by utilizing the tree-depth D.We create a new dataset by removing all inequalities with inference depth less than 4. We then randomly sample 1,200 problems and sort them by tree-depth in ascending order. For inequalities with the same tree-depth, they are sorted by the length of their string representation, with shorter lengths placed first.The fine-tuning procedure involves sequentially proving these inequalities and updating the parameters of the value network. If an inequality is successfully proved, we record the set of subgoals on the proof path as T and the set of subgoals that are searched but not on the proof path as F . The values of the elements in T are scaled down by a factor of ϵ, while the values of the elements in F are increased. Using these labels, we perform a training round on the value network V θ , and then proceed to the next problem. This iterative process is used to adjust the network parameters. See Appendix B.2 for more details.In this section, we provide details of our experiments and present the test results. We also include technical analysis of these results.We conduct a statistical analysis on the synthetic dataset, focusing on inequality lengths (in string representation) and tree-depth (the maximum expression tree height on both sides of an inequality), as depicted in Figure 5 . The distributions of lengths and tree-depth are related to the difficulty and search complexity. These distributions illustrate that our theorems range from simple to complex, reflecting a spectrum of difficulty levels in our dataset. The value network V θ comprises two main components: the pre-trained transformer encoder, Llemma-7b (Azerbayev et al. 2023) , followed by a 4096 × 256 × 1 multilayer perceptron that outputs a value in the interval (0, 1). Initially, AIPS successfully resolves 7 out of 20 problems from the test set using the pre-trained value network.The value network V θ functions as the heuristic in the best-first-search algorithm. It comprises two main components: the pre-trained transformer encoder, Llemma-7b, followed by a 4096 × 256 × 1 feedforward neural network that outputs a value in the interval (0, 1). Initially, AIPS successfully resolves 7 out of 20 problems from the test set using the pre-trained value network.The procedure of value curriculum learning is as follows. After successfully proving a theorem, each node along the proof path is relabeled with a value that is ϵ times its original value. For node that has been searched but is not part of the proof path, if its original label is v, the label of this node is updated at the end of this curriculum learning round according to the formula: max(m, v) × η + 1 -η.Here m represents the maximum value after modification among the proof path nodes. Subsequently, the relabeled nodes undergo 10 loops of fine-tuning training. We choose ϵ = 0.3 and η = 0.7.Before the value curriculum learning process, we randomly select 1,200 theorems from the synthetic dataset, excluding theorems with an inference depth of less than 4. These theorems undergo a curriculum learning strategy tailored for the pre-trained model. We limit the time for solving each problem to 40 minites. During curriculum learning, the theorems are solved and trained in an ascending order, sorted first by tree-depth, then by theorem length. The first 150 problems are solved within a mere two hours. After four days of training, AIPS solves 892 out of the first 1,000 problems, with 887 successes in the first 950 theorems. Since it struggles to solve problems after the 950th theorem, we decide to halt the training process at the 1,000th problem.The extensive experiments verify that the value curriculum learning strategy is very effective. The number of search loops required to solve testing theorems decreases noticeably throughout the training process, enabling AIPS to successfully solve 10 out of 20 IMO-level inequality problems using an RTX-4090 GPU and a single CPU. Fig. 6 shows the decreasing number of search loops during curriculum learning on the 2001 IMO Problem 2, and Fig. 7 shows the increasing number of solved problems during curriculum learning. We collect all ternary and quaternary algebraic inequality problems from IMO since 1990, some challenging problems from IMO shortlists and several national mathematical Olympiads, such as the USAMO, the USA National Team Selection Tests, the Polish/Korean/Japanese Mathematical Olympiad, all of which are of comparable difficulty to the IMO. The collected 20 problems provide a new challenging benchmark for the realm of automatic theorem proving, dubbed as MO- . The details of these 20 problems are as follows.• Problem 1 (IMO 1990 Shortlist) :For a > 0, b > 0, c > 0, d > 0 such that a • b + b • c + c • d + d • a = 1,show that:a 3 b + c + d + b 3 c + d + a + c 3 d + a + b + d 3 a + b + c ≥ 1 3 • Problem 2 (IMO 1993 Shortlist): For a > 0, b > 0, c > 0, d > 0,show that:a b + 2c + 3d + b 3a + c + 2d + c 2a + 3b + d + d a + 2b + 3c ≥ 2 3 • Problem 3 (IMO 1995 P2): For a > 0, b > 0, c > 0 such that a • b • c = 1, show that: 1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3 2 • Problem 4 (IMO 1996 Shortlist): For a > 0, b > 0, c > 0 such that a • b • c = 1, show that: a • b a 5 + a • b + b 5 + a • c a 5 + a • c + c 5 + b • c b 5 + b • c + c 5 ≤ 1 • Problem 5 (USAMO 1997 P5):For a > 0, b > 0, c > 0, show that:1 a 3 + b 3 + a • b • c + 1 b 3 + c 3 + a • b • c + 1 c 3 + a 3 + a • b • c ≤ 1 a • b • c • Problem 6 (IMO 1998 Shortlist A3):For a > 0, b > 0, c > 0 such that a • b • c = 1, show that:a 3 (1 + b)(1 + c) + b 3 (1 + c)(1 + a) + c 3 (1 + a)(1 + b) ≥ 3 4 • Problem 7 (IMO 2000 P2): For a > 0, b > 0, c > 0 such that a • b • c = 1, show that: (a -1 + 1 b )(b -1 + 1 c )(c -1 + 1 a ) ≤ 1 • Problem 8 (IMO 2001 P2): For a > 0, b > 0, c > 0, show that: a √ a 2 + 8bc + b √ 8ac + b 2 + c √ 8ab + c 2 ≥ 1 • Problem 9 (USAMO 2003 P5):For a > 0, b > 0, c > 0, show that:(a + b + 2c) 2 2c 2 + (a + b) 2 + (a + 2b + c) 2 2b 2 + (a + c) 2 + (2a + b + c) 2 2a 2 + (b + c) 2 ≤ 8 • Problem 10 (Poland 2004): For a > 0, b > 0, c > 0, d > 0, show that: a (a 3 + 63bcd) 1 3 + b (63acd + b 3 ) 1 3 + c (63abd + c 3 ) 1 3 + d (63abc + d 3 ) 1 3 ≥ 1 • Problem 11 (IMO 2004 Shortlist A5): For a > 0, b > 0, c > 0 such that a • b + b • c + c • a = 1, show that: 1 a + 6b 1 3 + 1 b + 6c 1 3 + 1 c + 6a 1 3 ≤ 1 a • b • c • Problem 12 (IMO 2006 P3):Given real numbers a, b, c, show that:|ab(a 2 -b 2 ) + bc(b 2 -c 2 ) + ca(c 2 -a 2 ))| ≤ 9 16 √ 2 (a 2 + b + c 2 ) 2 • Problem 13 (IMO 2009 Shortlist): For a > 0, b > 0, c > 0 such that 1 a + 1 b + 1 c = a + b + c, show that: (2a + b + c) -2 + (a + 2b + c) -2 + (a + b + 2c) -2 ≤ 16• Problem 14 (USA IMO Team Selection 2010 P2):For a > 0, b > 0, c > 0 such that a • b • c = 1, show that: 1 c 5 (a + 2b) 2 + 1 b 5 (2a + c) 2 + 1 a 5 (b + 2c) 2 ≥ 1 3 • Problem 15 (USAMO 2011 P1): For a > 0, b > 0, c > 0 such that a 2 + b 2 + c 2 + (a + b + c) 2 ≤ 4, show that: a • b + 1 (a + b) 2 + b • c + 1 (b + c) 2 + c • a + 1 (c + a) 2 ≥ 3• Problem 16 (Korea 2011 P4):For a ≥ 0, b ≥ 0, c ≥ 0 such that a + b + c = 1, show that:1 a 2 -4a + 9 + 1 b 2 -4b + 9 + 1 c 2 -4c + 9 ≤ 7 18• Problem 17 (USAMO 2012): For a > 0, b > 0, c > 0, show that:b 3 + 3c 3 5b + c + a 3 + 3b 3 5a + b + 3a 3 + c 3 a + 5c ≥ 2 3 (a 2 + b 2 + c 2 )• Problem 18 (Japan 2014 P5):For a ≥ 0, b ≥ 0, c ≥ 0 such that a + b + c = 1, show that: a 9bc + 4(b -c) 2 + 1 + b 9ac + 4(-a + c) 2 + 1 + c 9ab + 4(a -b) + 1 ≥ 1 2 • Problem 19 (USAMO 2017 P6): For a ≥ 0, b ≥ 0, c ≥ 0, d ≥ 0 such that a + b + c + d = 4, show that: a b 3 + 4 + b c 3 + 4 + c d 3 + 4 + d a 3 + 4 ≥ 2 3• Problem 20 (IMO 2020 P2):For a ≥ b, b ≥ c, c ≥ d, d > 0 such that a + b + c + d = 1, show that: (a + 2b + 3c + 4d)a a b b c c d d < 1 B.We evaluate the performance of Monte-Carlo Tree Search (MCTS). Compared to games like Go or chess, theorem proving can have an extremely large or even infinite action space, since applying each theorem or axiom usually comes with a set of parameters. Therefore, a direct application of MCTS to our problems is infeasible. To address this, we need to modify the MCTS algorithm.First, we place a restriction on our action space: at each state, we sample all possible actions generated from the current proof state, then sort them according to a tree-depth heuristic function, which evaluates the difficulty of the proof state after applying them, and pick the first k proof states (we choose k = 5). During the selection step in MCTS, we apply the Upper Confidence Bounds algorithm,SelectedAction = Argmax i   v i + C • ln(N ) n i  Here, n i is the number of visits of the i-th action (proof state), N is the number of visits of the current state, C is an adjustable hyperparameter (we choose C = 0.3 √ 2), and v i is the value of the state after applying the i-th action.We use two methods to compute v i : either it is directly given by the heuristic evaluation function, or we execute a best-first search to a constant depth d (d = 2), and take the value of the current best state as v i .Large Language Models (LLMs) currently struggle to solve IMO-level inequalities through the generation of natural language proofs. In our evaluation of 4 LLMs-GPT-4, GPT-4 Turbo, Gemini 1.5 Pro, and Llemma-7b-only Gemini 1.5 Pro successfully generates a correct solution to USAMO-1997-P5. Proofs generated by GPT-4 and GPT-4 Turbo contain some logical errors, while Llemma-7b rarely produces meaningful reasoning sentences. We present the results of first three LLMs below, including the only correct proof by Gemini 1.5 Pro to USAMO-1997-P5, and the incorrect proofs by using these three LLMs to IMO-1995-P2.Statement: (USAMO 1997 P5) Given three positive real numbers a, b, c, show that1 a 3 + b 3 + abc + 1 b 3 + c 3 + abc + 1 c 3 + a 3 + abc ≤ 1 abcCorrect proof:1. Factorization: Recall the factorization of the sum of cubes:x 3 + y 3 = (x + y)(x 2 -xy + y 2 )2. Apply AM-HM: For non-negative numbers x and y, the AM-HM inequality states:x + y 2 ≥ 2 1/x + 1/yRearranging the inequality:x 2 + y 2 -xy ≥ xy 3. Manipulate the given inequality: Lets focus on the first term and use the factorization:1 a 3 + b 3 + abc = 1 (a + b)(a 2 -ab + b 2 ) + abcSince a 2 -ab + b 2 ≥ ab (from step 2), we have:1 (a + b)(a 2 -ab + b 2 ) + abc ≤ 1 (a + b)ab + abc = 1 (a + b + c)ab4. Apply similar reasoning to other terms: Similarly, for the second and third terms:1 b 3 + c 3 + abc ≤ 1 (a + b + c)bc 1 c 3 + a 3 + abc ≤ 1 (a + b + c)ca 5.Combine the inequalities: Adding the three inequalities we just derived and simplify the right hand side:1 a 3 + b 3 + abc + 1 b 3 + c 3 + abc + 1 c 3 + a 3 + abc ≤ 1 abcThis completes the proof. 1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3/2Incorrect proof: (Generated by Gemini 1.5 Pro) Transformation: First, let's simplify the given expression by multiplying the numerator and denominator of each term by abc (which is equal to 1 due to the condition abc = 1):1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) = ab c 2 (a + b) + ac b 2 (a + c) + bc a 2 (b + c)Applying AM-HM: Now, consider the following positive numbers:x1 = c 2 (a + b), x2 = b 2 (a + c), x3 = a 2 (b + c)Applying AM-HM inequality to these:c 2 (a + b) + b 2 (a + c) + a 2 (b + c) 3 ≥ 3 1 c 3 (a+b) + 1 b 3 (a+c) + 1 a 3 (b+c)Simplifying: Expanding and simplifying the left side:a 2 b + ab 2 + ac 2 + a 2 c + b 2 c + bc 2 3 ≥ 3 ab c 2 (a+b) + ac b 2 (a+c) + bc a 2 (b+c)Since abc = 1, we can substitute and further simplify:ab/c + ac/b + bc/a 3 ≥ 3 1 c 3 (a+b) + 1 b 3 (a+c) + 1 a 3 (b+c)Final Step: Invert both sides of the inequality (remembering to flip the inequality sign):1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3/2This proves the required inequality.Figure 9 : Incorrect proof generated by Gemini 1.5 Pro. The errors are labeled in blue.Statement: (IMO 1995 P2) Given positive real numbers a, b, c such that abc = 1, show that1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3/2Incorrect proof: (Generated by ChatGPT4 Turbo) To prove this inequality, we can apply the AM-GM (Arithmetic Mean -Geometric Mean) inequality as follows:Given abc = 1: By applying the AM-GM inequality:a/b + b/a ≥ 2, b/c + c/b ≥ 2, c/a + a/c ≥ 2Summing these inequalities:(a/b + b/a) + (b/c + c/b) + (c/a + a/c) ≥ 6Rearrange and factor:a 2 /b 2 + b 2 /c 2 + c 2 /a 2 + b 2 /a 2 + c 2 /b 2 + a 2 /c 2 ≥ 6Now consider the expressions under the original inequality:1 a 3 (b + c) = 1 a 3 (b + c)Since abc = 1, we can write this as:= b 3 c 3 a 3 (b + c) = (bc) 3 a 3 (b + c) By AM-GM, b + c ≥ 2 √ bc.Therefore:1 a 3 (b + c) ≥ (bc) 3 2a 3 √ bc = b 2 c 2 2a 3 √ bc • √ bc = b 5/2 c 5/2 2a 3We can apply similar transformations to the other fractions:1 b 3 (c + a) ≥ a 5/2 c 5/2 2b 3 , 1 c 3 (a + b) ≥ a 5/2 b 5/2 2c 3Adding these up:1 a 3 (b + c) + 1 b 3 (c + a) + 1 c 3 (a + b) ≥ b 5/2 c 5/2 2a 3 + a 5/2 c 5/2 2b 3 + a 5/2 b 5/2 2c 3Using our earlier inequality(a 2 /b 2 + b 2 /a 2 + b 2 /c 2 + c 2 /b 2 + c 2 /a 2 + a 2 /c 2 ≥ 6)we can apply the generalized AM-GM inequality:1 a 3 (b + c) + 1 b 3 (c + a) + 1 c 3 (a + b) ≥ 1 2 • ( b 5/2 c 5/2 a 3 + a 5/2 c 5/2 b 3 + a 5/2 b 5/2 c 3 )Each of these terms is equal to 1 by our substitution using abc = 1, simplifying this expression:≥ 1/2 + 1/2 + 1/2 = 3/2Therefore, we have proved: Statement: (IMO 1995 P2) Given positive real numbers a, b, c such that abc = 1, show that1 a 3 (b + c) + 1 b 3 (c + a) + 1 c 3 (a + b) ≥ 3/21 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3/2Incorrect proof: (Generated by ChatGPT 4)The Arithmetic Mean -Geometric Mean (AM-GM) Inequality states:x1 + x2 + • • • + xn n ≥ n √ x1 • x2 . . . xn with equality if and only if x1 = x2 • • • = xn.Let's consider using AM-GM on the denominators.Analyzing Each Fraction For1 c 3 (a+b) : Since abc = 1, we have c 3 = 1 a 3 b 3 . Hence, 1 c 3 (a + b) = a 3 b 3 a + bSimiliarly:1 b 3 (a + c) = a 3 c 3 a + c , 1 a 3 (b + c) = b 3 c 3 b + cHere each fraction can be analyzed by using AM-GM on the denominators.a + b ≥ 2 √ ab, b + c ≥ 2 √ bc, c + a ≥ 2 √ caGiven abc = 1, we also have√ ab = c√ abc = c and similarly for others. Thus,a + b ≥ 2c, b + c ≥ 2a, c + a ≥ 2bSubstituting back:a 3 b 3 a + b ≥ a 3 b 3 2c , b 3 c 3 b + c ≥ b 3 c 3 2a , c 3 a 3 c + a ≥ c 3 a 3 2b Since a 3 b 3 = c 3 , b 3 c 3 = a 3 , c 3 a 3 = b 3 from abc = 1, a 3 b 3 2c = c 2 2 , b 3 c 3 2a = a 2 2 , c 3 a 3 2b = b 2 2 Adding these, a 2 2 + b 2 2 + c 2 2 = a 2 + b 2 + c 2 2To conclude, we need the final step:a 2 + b 2 + c 2 ≥ 3 which holds by AM-GM as a 2 + b 2 + c 2 ≥ 3 3 √ a 2 b 2 c 2 = 3.This completes the proof. We also test LeanCopilot (developed from LeanDojo Yang et al. (2024)) , the current open-source state-of-the-art theorem prover based on Lean. It solves none of the 20 problems, all resulting in time-limited feedback. We present some results of the tactic search provided by LeanCopilot in Figure 12 . It can be seen that the prover tends to rely heavily on built-in tactics and struggles to predict complex premises. When proving an inequality, AIPS first homogenizes both sides using the given conditions if the inequality is not already homogenized, thereby obtaining a new inequality. It then performs mixed reasoning on the new inequality to complete the proof. We present the proofs for the 10 problems solved by our AIPS as follows.1. Solution to IMO-1990-Shortlist Problem By <function try_homo>, It is equivalent to provea 3 b + c + d + b 3 a + c + d + c 3 a + b + d + d 3 a + b + c ≥ ab 3 + ad 3 + bc 3 + cd 3by <function check_AM_GM_Mul2>, it remains to provea 2 3 + b 2 3 + c 2 3 + d 2 3 ≤ a 3 b + c + d + b 3 a + c + d + c 3 a + b + d + d 3 a + b + cby <function try_together_l>, it remains to provea 2 + b 2 + c 2 + d 2 3 ≤ a 3 b + c + d + b 3 a + c + d + c 3 a + b + d + d 3 a + b + cwe use Hölder's inequality:(a 2 + b 2 + c 2 + d 2 ) 2 ≤ (a(b + c + d) + b(a + c + d) + c(a + b + d) + d(a + b + c))× (a 3 /(b + c + d) + b 3 /(a + c + d) + c 3 /(a + b + d) + d 3 /(a + b + c)).It remains to provea 2 + b 2 + c 2 + d 2 3 ≤ a 2 + b 2 + c 2 + d 2 2 a (b + c + d) + b (a + c + d) + c (a + b + d) + d (a + b + c)by <function all_cyc_mul_expr>, it remains to prove1 3 ≤ a 2 + b 2 + c 2 + d 2 a (b + c + d) + b (a + c + d) + c (a + b + d) + d (a + b + c) For f (x) = x 2 , f ′′ (x) > 0 for 0 < x.we use Jensen's inequality:4(a/4 + b/4 + c/4 + d/4) 2 ≤ a 2 + b 2 + c 2 + d 2 , it remains to prove 1 3 ≤ 4 a 4 + b 4 + c 4 + d 4 2 a (b + c + d) + b (a + c + d) + c (a + b + d) + d (a + b + c) For f (x) = x(a + b + c + d -x), f ′′ (x) < 0 for 0 < x < a + b + c + d, we use Jensen's inequality: a(b + c + d) + b(a + c + d) + c(a + b + d) + d(a + b + c) ≤ 4(a/4 + b/4 + c/4 + d/4)(3a/4 + 3b/4 + 3c/4 + 3d/4) it remains to prove 1 3 ≤ a 4 + b 4 + c 4 + d 4 3a 4 + 3b 4 + 3c 4 + 3d 4 by <function try_simp_r>, this is true! 2. Solution to IMO-1993-Shortlist problem. To prove a b + 2c + 3d + b 3a + c + 2d + c 2a + 3b + d + d a + 2b + 3c≥ 2 3 we use Hölder's inequality:(a + b + c + d) 2 ≤ ( a b + 2c + 3d ) + b 3a + c + 2d + c 2a + 3b + d + d a + 2b + 3c )× (a(b + 2c + 3d) + b(3a + c + 2d) + c(2a + 3b + d) + d(a + 2b + 3c)).It remains to prove2 3 ≤ (a + b + c + d) 2 4ab + 4ac + 4ad + 4bc + 4bd + 4cd by <function all_cyc_mul_expr>, it remains to prove 2 3 (a + b + c + d) 2 ≤ 1 4ab + 4ac + 4ad + 4bc + 4bd + 4cdby <function try_expand_l>, it remains to prove 2 3a 2 + 6ab + 6ac + 6ad + 3b 2 + 6bc + 6bd + 3c 2 + 6cd + 3d 2 ≤ 1 4ab + 4ac + 4ad + 4bc + 4bd + 4cd by <function nodiv_expr>, it remains to prove 8ab + 8ac + 8ad + 8bc + 8bd + 8cd ≤ 3a 2 + 6ab + 6ac + 6ad + 3b 2 + 6bc + 6bd + 3c 2 + 6cd + 3d 2 by <function zero_side>, it remains to prove0 ≤ 3a 2 -2ab -2ac -2ad + 3b 2 -2bc -2bd + 3c 2 -2cd + 3d 2 by <function check_AM_GM_Mul2>, it remains to prove 0 ≤ 2a 2 -2ab -2ad + 2b 2 -2bc + 2c 2 -2cd + 2d 2by <function check_AM_GM_Mul2>, this is true!a √ a 2 + 8bc + b √ 8ac + b 2 + c √ 8ab + c 2 ≥ 1,we use Hölder's inequality:(a + b + c) 3 ≤ a √ a 2 + 8bc + b √ 8ac + b 2 + c √ 8ab + c 2 2 a(a 2 + 8bc) + b(8ac + b 2 ) + c(8ab + c 2 ) .It remains to prove1 ≤ (a + b + c) 3 2 √ a 3 + 24abc + b 3 + c 3 .by <function all_cyc_mul_expr>, it remains to provea 3 + 24abc + b 3 + c 3 ≤ (a + b + c) 3 2by <function no_pow>, it remains to provea 3 + 24abc + b 3 + c 3 ≤ (a + b + c) 3by <function zero_side>, it remains to prove0 ≤ -a 3 -24abc -b 3 -c 3 + (a + b + c) 3by <function try_expand_r>, it remains to prove0 ≤ 3a 2 b + 3a 2 c + 3ab 2 -18abc + 3ac 2 + 3b 2 c + 3bc 2by <function check_AM_GM>, it remains to prove0 ≤ 3a 2 b -9abc + 3ac 2 + 3b 2 cby <function check_AM_GM>, this is true! 6. Solution to USAMO-2003-P5.To prove(a + b + 2c) 2 2c 2 + (a + b) 2 + (a + 2b + c) 2 2b 2 + (a + c) 2 + (2a + b + c) 2 2a 2 + (b + c) 2 ≤ 8 we have f (x) = (x + 1) 2 (1 -x) 2 + 2x 2 ≤ 12x + 4 3 for 0 < x < 1 ⇐⇒ - (3x -1) 2 • (4x + 1) 3 • (3x 2 -2x + 1) ≤ 0 for 0 < x < 1, which is true. Substitute x for c a + b + c, we have(a + b + 2c) 2 2c 2 + (a + b) 2 ≤ 4c a + b + c + 4 3 It remains to prove 4a a + b + c + 4b a + b + c + 4c a + b + c + 4 ≤ 8by <function try_together_l>, this is true!We select 10 synthetic problems generated by our AIPS for evaluation, and 4 IMO problems for comparison. Then, we invite three professional contestants to evaluate the difficulty and elegance of these 14 problems. Two of the evaluators are National Mathematical Olympiad gold medalists, and one is a silver medalist. The difficulty and elegance are needed to assign a score from 1 to 7, respectively.C.1 10 Synthetic Theorems and 4 Comparison IMO Problems C.1.1 10 Synthetic Theorems• (Problem1) Given a, b, c > 0, then (a + b + c) 3 (ab + bc + ca) 2 ≤ 4a (b + c) 2 + 4b (c + a) 2 + 4c (a + b) 2 • (Problem2) Given a, b, c > 0, then 27(a 2 + b 2 ) 2 (b 2 + c 2 ) 2 (c 2 + a 2 ) 2 (a 4 + b 4 + c 4 + 3a 2 b 2 + 3b 2 c 2 + 3c 2 a 2 ) 3 ≤ 1 • (Problem3) Given a, b, c > 0, then abc(a + b + c) 3 3(ab + bc + ca)(a 3 c + ab 3 + bc 3 ) ≤ 1 • (Problem4) Given a, b, c > 0, then 2a √ 2a 2 + b 2 + c 2 + 2b √ 2b 2 + c 2 + a 2 + 2c √ 2c 2 + a 2 + b 2 ≤ 3 √ 2(a + b + c) √ 5a 2 + 5b 2 + 5c 2 + ab + bc + ca • (Problem5) Given a, b, c > 0, then √ 6(a + b + c) 2 6 √ a 4 + b 4 + c 4 + a 2 b 2 + b 2 c 2 + c 2 a 2 ≤ a √ 2a 2 + b 2 + c 2 + b √ 2b 2 + c 2 + a 2 + c √ 2c 2 + a 2 + b 2 • (Problem6) Given a, b, c > 0, then 2(a + b + c) 3 2 ≤ ( √ a + b + √ b + c + √ c + a) √ a 2 + b 2 + c 2 + ab + bc + ca • (Problem7) Given a, b, c > 0, then (a 4 + b 4 + c 4 ) 3 2 √ ab 2 + bc 2 + ca 2 -abc √ a + b + c ≤ a 5 √ ca + b 2 + b 5 √ ab + c 2 + c 5 √ bc + a 2 • (Problem8) Given a, b, c > 0, then 54abc + (a + b + c) 3 √ a 2 + 2bc + √ 2ab + c 2 + √ 2ac + b 2 2 ≤ a + b + c • (Problem9) Given a, b, c > 0, then a 2 b (a + b) 3 + ac 2 (a + c) 3 + b 2 c (b + c) 3 ≤ 3 8 • (Problem10) Given a, b, c > 0, then (ab + ac + bc) 2 √ a 2 + b 2 + c 2 √ a 2 + b 2 + c 2 + 3ab + 3bc + 3ca ≤ a 2 b √ b 2 + 3ac + b 2 c √ c 2 + 3ab + c 2 a √ a 2 + 3bc C.1.2 4 IMO Problems • (1995-imo-2)Given a, b, c > 0 and abc = 1, then1 c 3 (a + b) + 1 b 3 (a + c) + 1 a 3 (b + c) ≥ 3 2 • (2001-imo-2) Given a, b, c > 0, then a √ a 2 + 8bc + b √ 8ac + b 2 + c √ 8ab + c 2 ≥ 1 • (2006-imo-3) Assume a, b, c are three real numbers, then |ab(a 2 -b 2 ) + bc(b 2 -c 2 ) + ca(c 2 -a 2 )| ≤ 9 16 √ 2 (a 2 + b 2 + c 2 ) 2 • (2020-imo-2) Assume a ≥ b ≥ c ≥ d ≥ 0 and a + b + c + d = 1, prove that a a b b c c d d (a + 2b + 3c + 4d) < 1 C.38th Conference on Neural Information Processing Systems (NeurIPS 2024).https://www.sympy.org/ 



Reviews: review: title: title: Review of "Proving Olympiad Algebraic Inequalities without Human Demonstrations"
main_review: main_review: Summary
* This work proposes a system for both generating complex inequality theorems (some up to IMO level) and solving Olympiad-level inequality problems without human demonstrations
* The system incorporates a value curriculum learning strategy on the generated datasets to improve performance

Strengths
* Results on both data generation and model performance are strong (generating a problem selected for a math olympiad and outperforming state-of-the-art methods in solving the problems)
* The value curriculum learning results show the novelty and importance of this approach
* Paper is clearly written and concise

Weaknesses
* Missing analysis of the limitations of AIPS, especially an analysis of the proofs that AIPS got incorrect. How close were the solutions produced by AIPS on the 10 problems it got wrong?
* It’s unclear to me whether the filtered synthetic data was only used for the AIPS results. If so, is it possible that fine tuning LLMs on this dataset could improve their performance? An interesting avenue for future work would be to explore how the synthetic data affects the performance of other model categories now that you have the ability to generate data more easily
* Minor errors: typo in Figure 5 caption, repeated sentences in B.2 paragraphs 1 and 2
title: title: Official Review
main_review: main_review: Summary: Much like the Euclidean geometry domain, the inequalities domain is also highly constrained and serves as a natural followup domain for an AlphaGeometry-style approach. The authors introduce AIPS, a collection of a symbolic deduction engine and a value network that, when looped in search, is capable of producing proofs to a fair number of olympiad inequality problems.

Significance: The work is significant; it seems to be a natural followup to AlphaGeometry. Similarly, the deductive engine is capable of most of the reasoning but the search tree must be constrained enough to reasonably find a proof. The value network operates somewhat similarly to the auxiliary-construction model from AG in this regard. The overall combined effort can solve some, but not all, inequality problems from popular olympiads. The synthetic problem generator appears to be quite valuable, especially as rated by professional contestants.

I think this would be a nice work for the MATH-AI community to see.

Q: How are the proofs checked? I may have missed this detail, but which proof assistant actually performs the checking? Is it a custom one for inequalities alone?
title: title: Could potentially be quite big for theorem proving dataset creation
main_review: main_review: ### Summary

The paper introduces **AIPS**, a model that autonomously generates and proves complex inequality theorems at the IMO level without human demonstrations. The system uses a symbolic deductive combined with a value network trained through curriculum learning to guide proof search efficiently. AIPS proves inequality theorems and outperforms state-of-the-art systems, solving 10 out of 20 Olympiad-level problems.

### Strengths

1. AIPS's ability to autonomously generate and prove Olympiad-level inequality theorems without human input is a major advancement in automated reasoning. This opens up possibilities for generating vast amounts of training data for theorem-proving systems.
2. The use of a value network trained through a curriculum learning strategy enables AIPS to improve its performance progressively, demonstrating efficient problem-solving strategies akin to human intuition. This method allows for better scalability and adaptability across problems of varying difficulty.
3. The paper demonstrates that AIPS outperforms previous state-of-the-art systems, solving 10 out of 20 IMO-level problems.
4. The system's ability to generate theorems that were used in real-world Olympiad competitions shows its potential for contributing novel and challenging mathematical problems for human mathematicians.
5. The paper provides a comprehensive evaluation of AIPS across various test sets and baselines, including comparisons with large language models (LLMs) and other formal theorem provers.

### Weaknesses

1. While AIPS excels in algebraic inequalities, the scope of the system is limited to this domain. It remains unclear how the system would generalize to other types of Olympiad-level mathematical problems, such as those involving geometry, number theory, or combinatorics.
2. The reliance on SymPy for symbolic manipulation introduces a potential bottleneck for more complex or non-standard inequalities, which may require specialized transformation rules beyond what SymPy currently supports.
3. Although the paper claims strong results, it does not provide a detailed breakdown of the computational resources required to run AIPS at scale. Given the complexity of proof searches, the system might face limitations in terms of computational efficiency when dealing with larger or more complex problem sets.
4. While AIPS outperforms previous models, the paper lacks a detailed analysis of its failure cases. Understanding where and why AIPS fails could help improve future iterations of the system and provide insights into its limitations.

### Questions

1. How would AIPS perform when applied to other mathematical domains beyond algebraic inequalities? Could its methodology be extended to handle problems from geometry or combinatorics?
2. What are the computational costs involved in running AIPS, especially on larger datasets or more complex problem sets? Are there ways to optimize the system for better efficiency?
3. How does AIPS handle ambiguities or non-standard forms of inequalities, particularly in real-world Olympiad problems that may not fit neatly into its predefined transformation rules?
4. Could the system be integrated with interactive theorem provers for further refinement of proofs, especially in cases where the generated proof may require additional human insight?
title: title: A Good Work that combines value networks with Sympy to prove IMO-level inequalties
main_review: main_review: This paper introduces AIPS, an approach for proving IMO-level inequalities. It first proposes automatically generating a large-scale dataset that contains complex cyclic symmetric inequalities by sampling from a predefined set of inequality theorems. A model is then fine-tuned on this dataset to serve as a value network, evaluating the difficulty of inequality expressions. This value network is combined with SymPy's symbolic deductive engine to perform a proof search. Experiments demonstrate that AIPS significantly outperforms a range of existing baselines, including pure LLMs and neural theorem provers, on 20 challenging IMO inequalities.

The paper is overall easy to read. While the high-level idea of this work is similar to prior work, the focus on inequality proving—a relatively underexplored domain in automated theorem proving—is a valuable contribution. The ability of AIPS to achieve 50% accuracy on IMO-level inequalities is noteworthy, given the complexity of these problems.

That said, the paper would benefit from structural improvements. The introduction is overly long, taking up too much space, while the methodology section is comparatively brief and lacks depth in some key areas. Shifting some of the content from the appendix to the main body, particularly details on the dataset generation process and the technical specifics of the value network, would provide a more balanced and informative presentation.