{"ID":3083743,"CreatedAt":"2026-06-05T06:46:15.197025399Z","UpdatedAt":"2026-06-07T07:23:37.79250861Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2606.06136","arxiv_id":"2606.06136","title":"A Finite Certificate for the Positive $n=9$ Vasc Inequality","abstract":"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.","short_abstract":"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-maxim...","url_abs":"https://arxiv.org/abs/2606.06136","url_pdf":"https://arxiv.org/pdf/2606.06136v1","authors":"[\"Dakai Guo\",\"Ruichen Qiu\",\"Yichuan Cao\",\"Ruyong Feng\"]","published":"2026-06-04T13:19:19Z","proceeding":"cs.SC","tasks":"[\"cs.SC\",\"cs.AI\"]","methods":"[]","has_code":false}