IneqAgent Uses LLMs and Symbolic Computation to Prove Inequalities in Lean

Summary

IneqAgent is an agentic framework for formal inequality proving in Lean4, where mathematical reasoning and exact symbolic computation must be connected through lemmas and reformulated goals. Its lemma-level Monte Carlo Tree Search coordinates lemma construction, goal reformulation, and the choice of symbolic backend. Sum-of-squares, Bernstein, and successive difference-substitution methods generate exact certificates for local Lean proofs, while Lean feedback helps combine these steps with LLM-generated reasoning into complete proofs checked against the original theorem statements. On four benchmarks, the configuration using DeepSeek-V4-Flash solved 175 of 186 problems, a 94.09% success rate and the highest overall rate among the evaluated methods. Across four backbone models, IneqAgent also achieved higher success rates than a Direct Agent at low inference-cost thresholds and had lower mean inference costs among successful runs. The authors report Lean-verified strengthenings of Dittert's conjecture in dimensions four and five, as well as a certificate for the Holens--Djokovic (4,4) inequality that implies Merris's conjecture in dimension four.