arXiv cs.AI· Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang·· 2 天前AI 评分34
IneqAgent：结合符号计算的 Lean 不等式证明智能体
IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
AI 导读
IneqAgent 是一个将 LLM 推理与符号计算结合、在 Lean4 中证明不等式的智能体框架，采用引理级蒙特卡洛树搜索协调引理构造、目标重写与符号后端选择。
正文 · 原文
Abstract: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 coordinates lemma construction, goal reformulation, and symbolic backend selection. Complementary sum-of-squares, Bernstein, and successive difference-substitution backends produce exact certificates for local Lean proof generation. The agent integrates these proofs with LLM-generated steps and uses Lean feedback to construct complete proofs checked against the original theorem statements. On four benchmarks, IneqAgent with DeepSeek-V4-Flash solves 175 of 186 problems (94.09%), achieving the highest overall success rate among the evaluated methods. Across four backbones, it achieves higher success rates at low LLM inference cost thresholds than Direct Agent using the same backbone, with lower mean inference costs over each method's successful runs. We also obtain Lean-verified strengthenings of Dittert's conjecture in dimensions four and five, and certify the Holens--Djokovic $(4,4)$ inequality, implying Merris's conjecture in dimension four.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.20681 [cs.AI] |
| (or arXiv:2610.20681v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.20681 arXiv-issued DOI via DataCite |
Submission history
From: Gaolei He [view email]
[v1]
Wed, 14 Oct 2026 16:29:11 UTC (203 KB)
来源：arXiv cs.AI · arxiv.org