IneqAgent 是一个面向 Lean4 的不等式证明框架，核心思想是将大语言模型（LLM）的推理能力与符号计算后端相结合。框架在引理层面采用 Monte Carlo Tree Search（MCTS），在搜索过程中动态决定是构造新引理、对目标进行重构，还是调用符号后端生成精确证书。
符号后端包括三类：
- 和平方（Sum‑of‑Squares）：将不等式转化为多项式的非负性问题，利用 SDP 求解得到证书；
- Bernstein 不等式：针对区间上的多项式，使用 Bernstein 基函数提供严格上界；
- 递进差分‑替换（Successive Difference‑Substitution）：通过逐步替换消除变量，实现局部不等式的直接验证。
每个后端都会输出 Lean 可接受的证书（如多项式系数或矩阵正定性证明），随后由 IneqAgent 将这些证书嵌入 LLM 生成的证明步骤中。Lean 的交互式反馈用于检验局部证明的正确性，并在必要时引导 MCTS 重新搜索。
在四个公开基准上，IneqAgent 搭配 DeepSeek‑V4‑Flash 解决了 175 / 186 个问题，成功率达 94.09%，超过所有对比方法。相同的 LLM 骨干下，IneqAgent 在低推理成本阈值下的成功率也高于直接代理（Direct Agent），且在成功运行的平均推理成本更低。
进一步的实验表明，IneqAgent 能够在 Lean 中验证 Dittert 猜想的四维和五维加强形式，并证实了 Holens‑Djokovic $(4,4)$ 不等式，从而在四维情形下推出 Merris 猜想。
点评：IneqAgent 展示了将 LLM 推理、搜索策略与符号计算深度融合的可行路径，为形式化不等式证明提供了高效且可验证的解决方案。