2 papers
cs.AI2026
IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
Gaolei He, Jinhui Li, Ruobing Zuo +2
Formal inequality proving requires mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. We introduce IneqAgent, an age…
cs.SC2026
A Proof of the Dittert Conjecture in Dimension 4 via an Exact Constrained Sum-of-Squares Certificate
Jinhui Li, Beibei Xiong, Zhengfeng Yang
The Dittert conjecture states that the Dittert functional on nonnegative matrices whose entries sum to is uniquely maximized by the uniform matrix. We prove the con…