# Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

arXiv: https://arxiv.org/abs/2502.13834 · HTML: https://mlsanity.com/paper/2502.13834/

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 35 of its 87 references that are in the map.
- First posted on arXiv 19 Feb 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 35)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Navigate through Enigmatic Labyrinth A Survey of Chain of Thought Reasoning: Advances, Frontiers and Future](https://mlsanity.com/paper/2309.15402/) (2023)
- [The Principles of Deep Learning Theory](https://mlsanity.com/paper/2106.10165/) (2021)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Sampling Can Be Faster Than Optimization](https://mlsanity.com/paper/1811.08413/) (2018)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Neuro-Symbolic Data Generation for Math Reasoning](https://mlsanity.com/paper/2412.04857/) (2024)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)

## Built on by (most cited first, 17 of 17)

- [RL Grokking Recipe: How Does RL Unlock and Transfer New Algorithms in LLMs?](https://mlsanity.com/paper/2509.21016/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning](https://mlsanity.com/paper/2505.23381/) (2025)
- [SciML Agents: Write the Solver, Not the Solution](https://mlsanity.com/paper/2509.09936/) (2025)
- [Foundation Models for Scientific Discovery: From Paradigm Enhancement to Paradigm Transition](https://mlsanity.com/paper/2510.15280/) (2025)
- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [Pre-trained Language Models Learn Remarkably Accurate Representations of Numbers](https://mlsanity.com/paper/2506.08966/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability](https://mlsanity.com/paper/2608.09538/) (2026)
- [Language Models Learn Universal Representations of Numbers and Here's Why You Should Care](https://mlsanity.com/paper/2510.26285/) (2025)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates](https://mlsanity.com/paper/2605.15445/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [REASON: Accelerating Probabilistic Logical Reasoning for Scalable Neuro-Symbolic Intelligence](https://mlsanity.com/paper/2601.20784/) (2026)
- [Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates](https://mlsanity.com/paper/2608.00326/) (2026)

## Abstract (arXiv)

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