2 papers
math.OC2026
Formal Safety Verification for Nonlinear Systems with Generative Barrier Certificate
Mengxin Ren, Hanrui Zhao
Safety verification is a fundamental problem in control theory. Barrier certificates (BCs) provide a powerful formal mechanism, yet deriving BCs is computationally intensive. This…
cs.AI2026
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…