IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

查看原文 / View Original 编辑 / Edit

Computer Science > Artificial Intelligence arXiv:2610.20681 (cs) [Submitted on 14 Oct 2026] Title:IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation Authors:Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang View a PDF of the paper titled IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation, by Gaolei He and 4 other authors View PDF HTML (experimental)

计算机科学 > 人工智能 arXiv:2610.20681 (cs) [提交于 2026 年 10 月 14 日] 标题：IneqAgent：Lean 中基于符号计算的智能不等式证明作者：Gaolei He, Jinhui Li, Ruobing Zuo, Xia Zeng, Zhengfeng Yang 查看标题为《IneqAgent：Lean 中基于符号计算的智能不等式证明》的论文 PDF，作者为 Gaolei He 及其他 4 位作者查看 PDF HTML（实验性）

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.

摘要：形式化不等式证明需要数学推理和精确计算，通常通过中间引理和目标重构来连接。我们引入了 IneqAgent，这是一个结合了大语言模型（LLM）推理与符号计算的智能框架，用于 Lean4 中的不等式证明。引理级蒙特卡洛树搜索协调了引理构建、目标重构以及符号后端的选择。

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.

互补的平方和（sum-of-squares）、伯恩斯坦（Bernstein）和连续差分代换后端为局部 Lean 证明生成提供了精确的证书。该智能体将这些证明与 LLM 生成的步骤相结合，并利用 Lean 的反馈来构建针对原始定理陈述进行校验的完整证明。

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.

在四个基准测试中，使用 DeepSeek-V4-Flash 的 IneqAgent 解决了 186 个问题中的 175 个（94.09%），在所有评估方法中实现了最高的总体成功率。在四个骨干模型中，它在低 LLM 推理成本阈值下比使用相同骨干模型的 Direct Agent 实现了更高的成功率，且在每种方法的成功运行中平均推理成本更低。

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.

我们还获得了在四维和五维空间中经 Lean 验证的 Dittert 猜想的加强版，并证明了 Holens—Djokovic $(4,4)$ 不等式，从而推导出了四维空间中的 Merris 猜想。