🤖 AI

A Finite Certificate for the Positive $n=9$ Vasc Inequality

This paper presents a human-guided AI-assisted proof of the positive-real $n=9$ case of the Vasc cyclic inequality, utilizing a finite certificate that verifies the inequality across all 40,320 sorted cones through a combination of polynomial reduction and automated verification.

Original authors: Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng

Published 2026-06-05

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a giant, complex puzzle made of numbers. For decades, mathematicians have been trying to solve a specific piece of this puzzle called the Vasc Inequality. Think of this inequality as a rule that says, "If you arrange these nine positive numbers in a circle and do a specific calculation with them, the result will always be zero or positive."

For a long time, we knew this rule worked for small groups of numbers (like 3, 4, or 5) and we knew it failed for some larger groups (like 6 or 13). But for the specific case of nine numbers, the answer was a mystery. It was the "missing link" in the chain.

This paper is the story of how a team of human mathematicians and an AI robot named MechMath finally solved the nine-number mystery.

The Problem: A Tangled Knot

The original math problem looks like a messy knot of fractions. It's hard to untangle because the numbers are in the bottom of the fractions (the denominators).

The Human Move: The team first "cleared the knot." They multiplied everything by the bottom parts of the fractions to turn the messy rule into a single, giant, smooth polynomial (a big math expression with no fractions). This made the problem much easier to look at, though still huge.

The Strategy: The "Maximum" and the "Sorted Line"

Even with the fractions gone, checking every possible combination of nine numbers is impossible. There are too many ways to arrange them.

The "Maximum" Trick: The team realized that because the numbers are in a circle, it doesn't matter where you start. You can always rotate the circle so the biggest number is at the top. This cuts the problem down significantly.
The "Sorted Line" Trick: Once the biggest number is fixed at the top, the team looked at the remaining eight numbers. They decided to check the rule only when these eight numbers are lined up from biggest to smallest.
The Combinatorial Explosion: Even with this trick, there are still 40,320 different ways to order those eight numbers (8 factorial). It's like trying to check 40,000 different keys to see if one opens a lock.

The Solution: The AI Agent and the "Certificate"

This is where the MechMath Agent Team (the AI) stepped in.

The Human Guide: The humans set up the rules and the strategy. They told the AI, "Here is the problem. Here is how we want to break it down."
The AI Worker: The AI did the heavy lifting. It wrote computer programs to split the 40,320 different orderings into tiny, manageable chunks.
The Certificate: Instead of writing out a 1,000-page proof that no one could read, the team created a Certificate. Think of this like a massive answer key or a receipt.
- For every single one of the 40,320 orderings, the AI generated a specific "proof leaf" (a tiny piece of evidence).
- Some leaves used a method called Polya Multipliers (like adding a safety net to the math).
- Some used AM-GM (a classic math shortcut that says the average of numbers is usually bigger than their product).
- Some just showed that all the numbers in the equation were positive.

The Verification: The Independent Auditor

The most important part of this paper isn't just that the AI found the answer; it's that the answer is trustworthy.

The humans didn't just take the AI's word for it. They built a separate, tiny, simple computer program (an independent verifier).
This verifier acted like a strict auditor. It looked at the "Certificate" (the answer key) and checked every single one of the 40,320 entries using basic, exact math.
It confirmed that for every single possible arrangement of the nine numbers, the math holds up.

The Result

The paper concludes that the rule is true for nine numbers.

The Scale: The final certificate is huge. It contains over 36,000 tiny proof pieces.
The Collaboration: It was a perfect dance between human logic (setting the stage and checking the work) and AI power (doing the millions of calculations).

In short, this paper didn't just solve a math problem; it demonstrated a new way to solve hard problems: Humans design the map, AI walks the path, and a simple, independent robot checks the footprints to make sure no one got lost. The "Nine-Number Vasc Inequality" is now officially solved.

Technical Summary: A Finite Certificate for the Positive $n = 9$ Vasc Inequality

Problem Statement
This paper addresses the positive-real case of the Vasc cyclic inequality for $n=9$ . The Vasc expression is defined as $C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$ with cyclic indexing. While the conjecture $C_n \ge 0$ has been proven for $n=3,4,5,7$ and disproven for $n=6, 13$ (and consequently all even $n \ge 6$ and odd $n \ge 13$ ), the cases for $n=9$ and $n=11$ remained open. Specifically, the $n=9$ case represents a critical frontier where previous Successive Difference Substitution (SDS) methods encounter a combinatorial explosion, requiring the analysis of $8! = 40,320$ distinct ordering regions.

Methodology
The proof strategy decouples human-verifiable algebraic reductions from a finite, machine-generated certificate. The workflow proceeds in five distinct stages:

Denominator Clearing: The rational inequality is transformed into a homogeneous polynomial inequality $P_9(x) \ge 0$ by multiplying by the positive product of all denominators, $D_9(x) = \prod (x_{i+1} + x_{i+2})$ .
Cyclic Maximum Reduction: Leveraging cyclic invariance, the verification domain is restricted to tuples where the first coordinate is the maximum ( $x_1 \ge x_i$ for all $i$ ).
Sorted Cone Parametrization: Within the fixed-maximum cone, the remaining eight variables are sorted according to all possible permutations ( $\sigma \in S_8$ ). This creates $40,320$ "sorted cones."
Gap Coordinate Transformation: Each sorted cone is parametrized using cumulative gap coordinates ( $y_1, \dots, y_9$ ), where $y_i \ge 0$ represents the difference between adjacent sorted variables. This maps the problem to a nonnegative orthant with a positive total gap.
Finite Certificate Verification: For each of the 40,320 sorted cones, a specific "terminal row" is generated. The validity of the inequality on each cone is established by verifying one of three soundness mechanisms:
- Coefficientwise Nonnegativity: All coefficients of the polynomial in gap coordinates are nonnegative.
- Polya Multiplier: The polynomial is multiplied by a positive factor (Polya multiplier) to yield a polynomial with nonnegative coefficients.
- AM-GM Midpoint Overlay: The polynomial is verified via Arithmetic Mean-Geometric Mean (AM-GM) circuit overlays.

Key Contributions and Execution
The primary contribution is the generation and verification of a finite exact certificate that covers the entire positive-real space for $n=9$ .

AI-Human Collaboration: The proof was obtained with human-guided assistance from the MechMath Agent Team, an LLM-driven agent. The agent autonomously executed the certificate verification phase, including writing Python verification programs, generating case splits, and organizing terminal classifications.
Certificate Scale: The published certificate contains 36,815 coefficient leaves, 2,236 ordinary Polya multiplier leaves, and 1,269 AM-GM midpoint overlay leaves.
Verification Rigor: The authors emphasize that the certificate is not a raw computational transcript but a formal artifact. It includes an independent verifier (written in Python using only the standard library) that recomputes fixed-maximum streams, polynomial hashes, and residual checks directly from the stored data, ensuring isolation from the code that generated the certificate.

Results
The paper successfully proves Theorem 1: For any positive real numbers $x_1, \dots, x_9$ , the inequality $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$ holds.

The proof resolves the first open entry in the status table of Vasc inequalities (Table 1).
The $n=11$ case remains open, with only partial positive results on a small cone currently available.

Significance
The paper claims significance in resolving a long-standing open problem in automated inequality proving that was previously blocked by combinatorial complexity. By demonstrating that a finite certificate can be generated and independently verified for a problem requiring the analysis of over 40,000 regions, the work validates a hybrid approach where AI agents handle the computational heavy lifting (case splitting, program generation, and verification) while human authors audit the mathematical reductions and verification logic. The work provides a reproducible route, including the certificate, an independent verifier, and a source rebuild path, establishing a new benchmark for the $n=9$ Vasc inequality.