IneqAgent：结合符号计算在 Lean 中证明不等式

用途与思路

根据该 arXiv 预印本摘要，IneqAgent 面向 Lean4 中的不等式形式化证明，把大模型推理与符号计算结合起来。其做法包括：在引理层面使用蒙特卡洛树搜索，协调引理构造、目标改写与符号后端选择；由平方和、Bernstein、逐次差分替换三类后端生成精确证书，用于本地 Lean 证明生成；再把符号证明与模型生成的步骤整合，并借助 Lean 的反馈构造可对原始定理陈述校验的完整证明。

报告结果

摘要在四个基准上评估，称 IneqAgent 配合 DeepSeek-V4-Flash 解决 186 道题中的 175 道，成功率 94.09%，在所评估方法中总体成功率最高。在四种骨干模型上，与使用相同骨干的 Direct Agent 相比，IneqAgent 在较低的 LLM 推理成本阈值下取得更高成功率，并在各自成功运行上的平均推理成本更低。摘要还提到得到 Dittert 猜想在四维和五维下经 Lean 验证的加强形式，并认证 Holens–Djokovic (4,4) 不等式，从而蕴含四维的 Merris 猜想。

限制与待核实

该资料为预印本摘要，未经同行评审，上述成功率和成本对比结论均未独立验证；摘要未给出基准名称、推理成本的具体计量方式、复现细节与代码可用性，这些内容需以原文或后续评审为准。