From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.

Proving mathematical inequalities is a foundational task in science and engineering. However, doing this automatically with computers is incredibly difficult. Traditional software relies on rigid logic that slows down when math problems become large and complex. Meanwhile, modern Large Language Models are great at guessing solutions but cannot guarantee absolute mathematical accuracy. To solve this, we introduce NSPI, a new framework that combines AI intuition with strict mathematical checking. In our system, the AI first suggests a smart blueprint for why an inequality might be true. Then, a traditional mathematical tool takes this suggestion, fixes any minor errors, and converts it into a bulletproof proof that a computer can independently verify. Our method successfully proves complex mathematical inequalities with up to 10 variables, outperforming previous automated techniques and paving the way for more reliable AI assistants in advanced mathematics.