Elamur Research⌕
☰
home / papers / 2025 / Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

Paper · 2025 · Zenan Li, Zhaoyu Li, Wen Tang et al.

Summary

The paper tackles automated formal proving of elementary algebraic inequalities from math Olympiads. Pure LLM provers struggle because formal proof data is scarce and the tactic space is huge. Symbolic methods such as cylindrical algebraic decomposition scale poorly and give opaque, non-readable proofs. The authors present LIPS, a neuro-symbolic prover working in Lean.

LIPS is built from an analysis of how humans solve such problems, which it splits into two tactic families:

  • Scaling applies a known lemma such as AM-GM or Cauchy-Schwarz. Symbolic tools enumerate these exhaustively, and an SMT solver discards any step that makes the goal false.
  • Rewriting produces equivalent transformations. LLMs propose these through format-specific prompts.

The resulting subgoals are pruned with symbolic heuristics based on homogeneity and decoupling. An LLM then ranks the survivors using chain-of-thought.

On 161 competition inequalities, LIPS reaches state-of-the-art results without any extra training data, beating both neural and symbolic baselines in success rate and speed. Its output is a human-readable proof that Lean verifies. This shows that dividing reasoning carefully between LLMs and symbolic engines can make up for limited data.

Key points

  • Benchmark: 161 inequalities collected from a trio of sources: the problem collections of Chen (2014) and Tung (2012), along with the AIPS set of Wei et al. (2024).
  • Main result: on the 61 Olympiad-sourced problems, LIPS proves 56 within 90 minutes. The previous best method proves 41 and gives no human-readable proofs.
  • Tactic split: symbolic scaling uses lemma applications such as NEQ_AM_GM_... and NEQ_Cauchy_Schwarz_..., plus Muirhead and the tangent-line trick. LLM rewriting uses tactics such as llm_simplify, llm_rearrange and llm_cancel_denom.
  • No fine-tuning: unlike INT and AIPS, LIPS needs no synthetic training data. It combines off-the-shelf LLMs with SMT/CAD-style solvers.
  • Error detection: the symbolic counterexample search found flaws in community solutions posted on AoPS, for example for the Japan 1997 problem.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 4,145 worksReasoning · 1,948 works

Cite

Cite as Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang and Xiaoxing Ma. 2025. Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning. arXiv:2502.13834.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2502.13834 · arXiv 2502.13834

@misc{li2025proving,
  title = {{Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning}},
  author = {Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang and Xiaoxing Ma},
  year = {2025},
  doi = {10.48550/arxiv.2502.13834},
  eprint = {2502.13834},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2502.13834}
}

References

85 references, 29 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Meta AI. Llama 3 model card. 2024. URL https://github.com/meta-llama/llama3/ blob/main/MODEL_CARD.md. ↗
  2. Dennis S Arnon, George E Collins, and Scott McCallum. Cylindrical algebraic decomposition I: The basic algorithm. SIAM Journal on Computing, 1984. find
  3. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength SMT solver. In International Conference on Tools and Algorithms for the Construction and Analys…
  4. Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. 2018. find
  5. Lasse Blaauwbroek, 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 on Machine Learning (ICML), 2024.
  6. Bob F Caviness and Jeremy R Johnson. Quantifier elimination and cylindrical algebraic decomposition. Springer Science & Business Media, 2012. find
  7. Evan Chen. Supersums of square-weights (SOS), 2013. find
  8. Evan Chen. A brief introduction to olympiad inequalities. evanchen.cc/handouts/Ineq/en.pdf. 2014. find
  9. URL https://web. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 2000. find
  10. 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 arXiv:2309.15402, 2023.
  11. Project Coq. The Coq proof assistant-reference manual. INRIA Rocquencourt and ENS Lyon, version, 5, 1996. find
  12. James H Davenport and Joos Heintz. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation, 1988. find
  13. Leonardo De Moura and Nikolaj Bjørner. Efficient e-matching for SMT solvers. In Automated Deduction–CADE-21: 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings 21, pp. 183–198. find
  14. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008. find
  15. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction (CADE), 2015. find
  16. DeepSeek-AI. DeepSeek-V2: A strong, economical, and efficient mixture-of-experts language model, 2024. find
  17. Amir Dembo, Thomas M Cover, and Joy A Thomas. Information theoretic inequalities. IEEE Transactions on Information theory, 1991. find
  18. 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.
  19. Zhoulai Fu and Zhendong Su. XSat: A fast floating-point satisfiability solver. In International Conference on Computer Aided Verification (CAV), 2016. find
  20. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Learning to reason with HOL4 tactics. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017. find
  21. Georges Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In Proceedings of the Asian Symposium on Computer Mathematics, 2008. find
  22. Google DeepMind. AI achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ ai-solves-imo-problems-at-silver-medal-level/, 2024. ↗
  23. 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.
  24. Kristian J Hammond and David B Leake. Large language models need symbolic AI. In International Workshop on Neural-Symbolic Learning and Reasoning,, 2023. find
  25. 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.
  26. Godfrey Harold Hardy, John Edensor Littlewood, and George Pólya. Inequalities. 1952. find
  27. André Heck and Wolfram Koepf. Introduction to Maple. 1993. find
  28. 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. find
  29. Bruce Ikenaga. Techniques in proving inequalities, Sep 2018. URL https://sites.millersville.edu/bikenaga/math-proof/inequalities/inequalities. html. ↗
  30. 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. find
  31. 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. In International Conference on Learning Representations (ICLR), 2023b.
  32. Mats Jirstrand. Cylindrical algebraic decomposition-an introduction. Linköping University, 1995. find
  33. Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. ACM Communications in Computer Algebra, 2013. find
  34. Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carlo planning. In European conference on machine learning, 2006. find
  35. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification (CAV), 2013. find
  36. Gereon Kremer. Cylindrical algebraic decomposition for nonlinear arithmetic problems. PhD thesis, Dissertation, RWTH Aachen University, 2020, 2020. find
  37. Gereon Kremer, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). In International Joint Conference on Automated Reasoning, 2022. find
  38. 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.
  39. Hojoo Lee. Topics in inequalities-theorems and techniques. Korea Institute for Advanced Study, Seoul, 2004. find
  40. François Lemaire, M Moreno Maza, and Yuzhen Xie. The regularchains library in Maple. ACM SIGSAM Bulletin, 2005. find
  41. Kin-Yin Li. Using tangent lines to prove inequalities. Mathematical Excalibur, 2006:1, 2005. find
  42. 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, 37:23488–23515, 2025.
  43. 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.
  44. 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.07640, 2025.
  45. Nelson F 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.
  46. Yang Lu. Practical automated reasoning on inequalities: Generic programs for inequality proving and discovering. Asian Technology Conference in Mathematics, 1998. find
  47. 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. find
  48. Radmila Bulajich Manfrino, José Antonio Gómez Ortega, and Rogelio Valdez Delgado. Inequalities: a mathematical olympiad approach. 2010. find
  49. Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondřej Čertı́k, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. SymPy: symbolic computing in python. PeerJ Computer Science, 2017. find
  50. Michał Moskal, Jakub Łopuszański, and Joseph R Kiniry. E-matching for fun and profit. Electronic Notes in Theoretical Computer Science, 198(2):19–35, 2008. find
  51. Yurii Nesterov. Introductory lectures on convex optimization: A basic course. 2013. find
  52. Allen Newell and Herbert Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 1956. — The logic theory machine: A complex information processing system
  53. Xinpeng Ni, Yulun Wu, and Bican Xia. Solving SMT over non-linear real arithmetic via numerical sampling and symbolic verification. In International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, 2023. find
  54. Lawrence C Paulson. Isabelle: A Generic Theorem Prover. 1994. find
  55. Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selection for Lean. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2023. find
  56. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  57. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal Mathematics Statement Curriculum Learning. In International Conference on Learning Representations (ICLR), 2023.
  58. Daniel A Roberts, Sho Yaida, and Boris Hanin. The principles of deep learning theory. Cambridge University Press Cambridge, MA, USA, 2022. find
  59. Stephan Schulz. E–a brainiac theorem prover. AI Communications, 2002. find
  60. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024. find
  61. 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.
  62. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 2024.
  63. Nguyen Duy Tung. 567 nice and hard inequality. https://phamtuankhai.wordpress.com/wp-content/uploads/2012/04/567-bat-dang-thuc-hay.pdf, April 2012. ↗
  64. Ali K Uncu, James H Davenport, and Matthew England. SMT-solving induction proofs of inequalities. arXiv preprint arXiv:2307.16761, 2023. — [arXiv:2307.16761](https://arxiv.org/abs/2307.16761) find
  65. Marcell János Uray. On proving inequalities by cylindrical algebraic decomposition. In Annales Universitatis Scientiarum Budapestinensis de Rolando Eotvos Nominatae. Sectio Computatorica, 2020. find
  66. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1—machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, 2008. find
  67. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Neural Information Processing Systems (NeurIPS), 2017.
  68. Pauli Virtanen, Ralf Gommers, Travis E Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, et al. SciPy 1.0: fundamental algorithms for scientific computing in Python. Nature methods, 2020. — SciPy 1.0 — Fundamental Algorithms for Scientific Computing in Python
  69. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et 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…
  70. Chenrui Wei, Mengzhou Sun, and Wei Wang. Proving olympiad algebraic inequalities without human demonstrations. In Neural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2024.
  71. 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.
  72. 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(POPL), January 2021. doi: 10.1145/3434304. URL https://doi.org/10.1145/3434304. ↗
  73. Wolfram Research. mathematica. Mathematica, version 14.1. URL https://www.wolfram.com/ ↗
  74. Wolfram Research. Cylindrical Decomposition, 2020. URL https://reference.wolfram.com/language/ref/CylindricalDecomposition.html. ↗
  75. Wen-tsün Wu. On the decision problem and the mechanization of theorem-proving in elementary geometry. In Selected Works Of Wen-Tsun Wu, pp. 117–138. World Scientific, 2008. find
  76. Yuhuai Wu, Albert Q Jiang, Jimmy Ba, and Roger Grosse. INT: An inequality benchmark for evaluating generalization in theorem proving. In International Conference on Learning Representations (ICLR), 2021.
  77. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  78. 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.
  79. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023.
  80. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI. arXiv preprint arXiv:2412.16075, 2024.
  81. Lu Yang. Recent advances in automated theorem proving on inequalities. Journal of Computer Science and Technology, 1999. find
  82. 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.03847, 2024.
  83. Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Cezary Kaliszyk, and Josef Urban. Online machine learning techniques for Coq: a comparison. In International Conference on Intelligent Computer Mathematics, 2021. find
  84. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-Based Demonstration Learning for Formal Theorem Proving. In International Conference on Machine Learning (ICML), 2024. find
  85. 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.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/li-2025-proving-olympiad-inequalities-synergizing-llms/