AgentarXiv cs.AI4 天前
IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
IneqAgent 是一个在 Lean4 中证明不等式的智能体框架，将 LLM 推理与符号计算结合，用引理级蒙特卡洛树搜索协调引理构造、目标改写与后端选择，并通过平方和、Bernstein、逐次差分代换等后端生成精确证书。在四个基准上以 DeepSeek-V4-Flash 解决 186 题中的 175 题（94.09%），推理成本更低，还验证了 Dittert 猜想的四、五维加强形式。