IneqAgent：结合符号计算在 Lean 中实现智能体不等式证明

研究人员提出 IneqAgent，这是一个将大语言模型推理与符号计算相结合的智能体框架，用于在 Lean4 中进行不等式证明。它利用引理级蒙特卡洛树搜索协调引理构建与后端选择，并借助平方和、Bernstein 等符号后端生成证明凭证。结合 DeepSeek-V4-Flash 时，该方法在 4 个基准测试中解决 186 道题目中的 175 道（94.09%），以更低的平均推理成本取得了最高总成功率。