IneqAgent: LLM-guided agent for inequality proving in Lean4
IneqAgent is an agentic framework that combines LLM reasoning with symbolic computation to prove inequalities in Lean4. It uses lemma-level Monte Carlo Tree Search to coordinate lemma construction, goal reformulation, and selection among exact-symbolic backends (sum-of-squares, Bernstein, successive difference-substitution); on four benchmarks with DeepSeek-V4-Flash it solves 175 of 186 problems (94.09%) and produces Lean-verified strengthenings of Dittert's conjecture (dimensions 4 and 5) and a certification of the Holens--Djokovic (4,4) inequality.