IneqAgent is an agentic framework for inequality proving in Lean4 that tightly couples large language model (LLM) reasoning with symbolic computation backends. At the lemma level it runs a Monte Carlo Tree Search (MCTS) that decides whether to construct a new lemma, reformulate the goal, or invoke a symbolic backend to produce an exact certificate.
Three symbolic backends are supported:
- Sum‑of‑Squares: transforms the inequality into a polynomial non‑negativity problem and obtains a certificate via semidefinite programming;
- Bernstein: provides rigorous upper bounds for polynomial inequalities on intervals using Bernstein basis functions;
- Successive Difference‑Substitution: eliminates variables step‑by‑step, yielding direct local proofs.
Each backend outputs a Lean‑compatible certificate (e.g., polynomial coefficients or a positive‑definite matrix proof). IneqAgent then weaves these certificates into the proof steps generated by the LLM. Interactive Lean feedback checks the validity of local proofs and, when necessary, guides the MCTS to explore alternative branches.
On four public benchmarks, IneqAgent paired with DeepSeek‑V4‑Flash solves 175 out of 186 problems (94.09% success), outperforming all evaluated baselines. With the same LLM backbone, IneqAgent achieves higher success rates at low inference‑cost thresholds than the Direct Agent and exhibits lower mean inference cost across successful runs.
Additional experiments show that IneqAgent can produce Lean‑verified strengthenings of Dittert’s conjecture in dimensions four and five, and certify the Holens‑Djokovic $(4,4)$ inequality, which implies Merris’s conjecture in dimension four.
Review: IneqAgent demonstrates a practical pathway for integrating LLM reasoning, search strategies, and symbolic computation, delivering an efficient and formally verified solution for inequality proving.