A Finite Certificate for the Positive $n=9$ Vasc Inequality
This solves a long-standing open case of a known inequality, but the method is specific to this problem and not broadly applicable.
The paper proves the positive-real n=9 case of the Vasc cyclic inequality using a human-guided AI approach, resulting in a finite certificate with 36815 coefficient leaves, 2236 Polya multiplier leaves, and 1269 AM-GM overlay leaves.
We prove the positive-real $n=9$ case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all $8!=40320$ sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has $36815$ coefficient leaves, $2236$ ordinary Polya multiplier leaves, and $1269$ AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.