IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
Formal inequality proving requires mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. We introduce IneqAgent, an agentic framework combining LLM reasoning with symbolic computation for inequality proving in Lean4. Lemma-level Monte Carlo Tree Search coordi...
Gao-Lei He, Jin-Hui Li, Ruo-Bing Zuo et al.
· 0 citations