IneqAgent 把 MCTS 与 SOS / Bernstein 等符号证书接入 Lean：186 题解出 175 题，并得到新 inequality strengthenings

He 等提出 IneqAgent，把 LLM 推理与精确 symbolic computation 组合成 Lean 4 inequality prover：lemma-level Monte Carlo Tree Search 协调 lemma construction、goal reformulation 与 backend selection，sum-of-squares、Bernstein 与 successive difference-substitution 等后端生成局部精确证书，再由 LLM 与 Lean feedback 组装完整证明。论文报告 DeepSeek-V4-Flash 配置在四个 benchmark 上解出 175/186（94.09%），并在四种 backbone 上相较相同模型的 Direct Agent 呈现更好的低推理成本 success-rate。除 benchmark 外，系统还得到并 Lean 验证 Dittert conjecture 在维数 4、5 的 strengthenings，并认证 Holens–Djokovic (4,4) inequality，从而推出四维 Merris conjecture。