5 papers · 1 filter
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…
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…
Richer Representations for Neural Algorithmic Reasoning via Auxiliary Reconstruction
Jiafu Huang, Chao Peng, Chenyang Xu +7
Neural algorithmic reasoning has emerged as a popular research direction. It aims to train neural networks to mimic the step-by-step behavior of classical rule-based algorithms. Mo…
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
Ruobing Zuo, Hanrui Zhao, Gaolei He +2
Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search…
Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
Beibei Xiong, Hangyu Lv, Junqi Liu +5
Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Sym…