1
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
提出用LLM生成猜想并转化为Lean形式化验证，基于平方和证书实现自动多项式不等式证明，开辟数学推理新路径。
arXiv:2605.15445v1 Announce Type: new Abstract: Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reas…