Exact proof certificates for 11-variable inequality verified in Lean
Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality
Symbolic Computation
Summary
The paper proves that a complicated expression involving eleven positive numbers is never negative. To do this, the authors turn the problem into showing a related polynomial is always nonnegative. They provide exact, rational certificates—like mathematical proof-checks in matrix form—to confirm this fact. These certificates are rigorously verified using a formal system called Lean, ensuring no mistakes. The detailed proof and data are made publicly available for anyone to verify.
What this means in practice
- •For software verification teams: Use formalized certificates and Lean verification to ensure correctness of complex polynomial inequalities in software systems.
- •For computer algebra system developers: Incorporate exact rational certificate methods to improve automated proofs of polynomial inequalities within algebraic software tools.
A theory result. No direct application yet.
Authors
Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao
Abstract
We prove that the cyclic sum $\sum_{i=0}^{10}(x_i-x_{i+1})/(x_{i+1}+x_{i+2})$ is nonnegative for every strictly positive real eleven-tuple, with indices taken modulo eleven. Clearing denominators reduces the problem to a homogeneous polynomial. Subtracting the smallest coordinate then separates the proof into nonnegativity of a common-translation derivative and nonnegativity on a full boundary face. We supply exact rational polynomial certificates in Gram-matrix form for both statements. The derivative certificate uses a linear multiplier, centered monomials and cyclic averaging; the boundary certificate uses a strictly positive quadratic multiplier and uncentered monomials. Their verification requires 6,069 cyclic coefficient comparisons and 34,304 literal coefficient comparisons. All 606 certificate matrices are certified by integer congruences with strictly diagonally dominant images. A Lean 4 development formally verifies the certificate checks and their connection to the original inequality. The exact certificate data, replay programs, and formal sources are publicly available.