Machine Proofs of Homogeneous Polynomial Inequalities (Difference Substitution)

齐次多项式不等式的机器证明（差分代换） 苏剑林 · 2014-07-06 · Mathematics proof inequality symmetry

Back in high school, like many students, I took part in math competitions, and while preparing for them I worked through plenty of competition problems—inequality proofs, of course, being a staple of that genre. At the time, whenever I was confronted with all sorts of inequality-proving problems, I always felt rather lost: after looking at the answer, the construction of the proof always seemed marvelously clever, yet whenever I tried to come up with it myself, I could never quite manage it. So the idea occurred to me: "Is there a general-purpose way to prove these inequalities?" To achieve this, I came up with the technique described in this post—trading off computational simplicity for a proof method that's guaranteed to work. Later on, although I never ended up pursuing math competitions as a path, I kept this method in my back pocket, and recently, while discussing inequality problems with friends on a math research forum, I picked it back up again.

I've mentioned this technique before, in the earlier blog post "A 'Physical Proof' of Symmetric Polynomial Inequalities"], but back then, limited by what I knew at the time, my understanding of it wasn't very deep. In this post, I'll expand on it further. I originally discovered this technique independently while working on proofs myself, but when I searched around online, I found that earlier researchers (Yang Lu, Yao Yong, Yang Xuezhi, and others) had already studied this technique long ago, calling it "difference substitution," and had already explored its role in machine-generated proofs. This technique can be used quite generally for proving homogeneous/non-homogeneous inequalities; for reasons of space, this post will only discuss homogeneous polynomial inequalities—specifically, symmetric homogeneous polynomial inequalities—and I've found a few places where the process can be simplified. more

A Basic Example

To open, let's take the well-worn AM-GM inequality

$$a^3+b^3+c^3\geq 3abc,\quad \forall a,b,c \geq 0$$

as our illustrative example. There are many elegant ways to prove the AM-GM inequality, such as in "Two Clever Proofs of the AM-GM Inequality"]. Here, we'll instead give an "inelegant" proof using difference substitution. The technique of difference substitution is to assume $a\leq b\leq c$, and then use the following substitution:

$$\begin{aligned}a&=a\\ b&=a+u\\ c&=a+u+v \end{aligned}\quad \forall a,u,v \geq 0$$

which gives

$$\begin{aligned}&a^3+b^3+c^3-3abc\\ =&a^3+(a+u)^3+(a+u+v)^3-3a(a+u)(a+u+v)\\ =&3 a u^2+3 a u v+3 a v^2+2 u^3+3 u^2 v+3 u v^2+v^3\end{aligned}$$

Since every coefficient of every term in the final equality is positive, it is clearly nonnegative, and so the inequality holds.

The same technique can be applied to non-symmetric inequalities, such as $f(a,b,c)\geq 0$, where equality is required to hold at $a=b=c$. However, since $a,b,c$ is not symmetric, we'd need to apply the same method separately to every possible ordering of $a,b,c$ (six orderings in total, i.e., by enumeration). The role that symmetry plays is precisely to reduce the number of cases we need to enumerate—for instance, if there is a cyclic symmetry (also called rotational symmetry), the number of cases to check drops to 2, and if, as in the example above, there is full symmetry, only a single check is needed. Since the calculations involve extensive polynomial expansion—especially with many variables or high degrees—doing this by hand is often infeasible. This is why the difference substitution technique is particularly well suited to machine-generated proofs, letting software handle the complicated expansions.

The difference substitution technique has a very broad range of applicability. Let's look at an inequality from the shortlist of the 31st IMO:

$$(a^2+ab+b^2)(b^2+bc+c^2)(c^2+ca+a^2)\geq (ab+bc+ca)^3$$

This is a fully symmetric inequality, meaning it's unchanged under swapping any two variables, so we may assume $a\leq b\leq c$. Setting $b=a+u,c=a+u+v$, we get

$$\begin{aligned}&f(a,b,c)\\ =&(a^2+ab+b^2)(b^2+bc+c^2)(c^2+ca+a^2)-(ab+bc+ca)^3\\ =&9 a^4 u^2 + 26 a^3 u^3 + 27 a^2 u^4 + 12 a u^5 + 2 u^6 + 9 a^4 u v + \\ &39 a^3 u^2 v + 54 a^2 u^3 v + 30 a u^4 v + 6 u^5 v + 9 a^4 v^2 + \\ &33 a^3 u v^2 + 48 a^2 u^2 v^2 + 30 a u^3 v^2 + 7 u^4 v^2 + \\ &10 a^3 v^3 + 21 a^2 u v^3 + 15 a u^2 v^3 + 4 u^3 v^3 + 3 a^2 v^4 + \\ &3 a u v^4 + u^2 v^4\end{aligned}$$

Long and messy, indeed—this was expanded using Mathematica, and I don't expect any student to use a technique like this in an exam room. But difference substitution really is an effective proof technique: as we can see, in the final expansion, all the coefficients are positive, so the inequality obviously holds.

I've since checked many similar fully symmetric inequalities and found that the proof succeeds every time; and, to my surprise, I have yet to find a fully symmetric inequality whose final expansion contains a negative coefficient.

Cyclic Symmetric Inequalities

In this section, we prove the following cyclic inequality:

$$4(a+b+c)^3 \geq 27(ab^2+bc^2+ca^2+abc),\quad \forall a,b,c\geq 0$$

This problem is not fully symmetric; it has only a cyclic symmetry—that is, it remains invariant under

$$\begin{aligned}&(a,b,c)\to(b,c,a)\\ &(a,b,c)\to(c,a,b)\end{aligned}$$

This lets us fix which variable is the minimum—say $a$—and then check the two cases $a\leq b\leq c$ and $a\leq c\leq b$ separately.

First, write $F(a,b,c)=4(a+b+c)^3-27(ab^2+bc^2+ca^2+abc)$. For $a\leq b\leq c$, set $b=a+u,c=a+u+v$, and we get

$$\begin{aligned}&F(a,a+u,a+u+v)\\ =&9 a u^2 + 5 u^3 + 9 a u v - 6 u^2 v + 9 a v^2 - 3 u v^2 + 4 v^3\end{aligned}$$

Hm? A negative coefficient has shown up? Not hard to deal with, though. We know that $a$ can be arbitrarily large, while $u,v$ can be arbitrarily close to 0, and equality in the inequality holds at $u=v=0$; the degree of $a$ effectively represents the "order" of each term. To handle the negative-sign term, we group terms of the same order together:

$$\begin{aligned}&F(a,a+u,a+u+v)\\ =&9 a u^2 + 5 u^3 + 9 a u v - 6 u^2 v + 9 a v^2 - 3 u v^2 + 4 v^3\\ =&9 a (u^2+uv+v^2) + (5 u^3 - 6 u^2 v - 3 u v^2 + 4 v^3)\end{aligned}$$

and it only remains to note that $5 u^3 - 6 u^2 v - 3 u v^2 + 4 v^3=(u - v)^2 (5 u + 4 v)$, which completes the proof for this case.

For the other case, $a\leq c\leq b$, set $c=a+u,b=a+u+v$, and we get

$$\begin{aligned}&F(a,a+u+v,a+u)\\ =&9 a u^2 + 5 u^3 + 9 a u v + 21 u^2 v + 9 a v^2 + 24 u v^2 + 4 v^3\end{aligned}$$

which is the simple case where all coefficients are positive, completing the proof.

Now let's prove a much more formidable inequality:

$$\frac{1}{4}\left(\frac{a^2}{b}+\frac{b^2}{c}+\frac{c^2}{d}+\frac{d^2}{a}\right)\geq \sqrt{\frac{a^4+b^4+c^4+d^4}{4}},\forall a,b,c,d\geq 0$$

This problem is also cyclically symmetric. It can be reformulated as proving the nonnegativity of

$$f(a,b,c,d)=\left[\frac{1}{4}\left(\frac{a^2}{b}+\frac{b^2}{c}+\frac{c^2}{d}+\frac{d^2}{a}\right)\right]^4-\frac{a^4+b^4+c^4+d^4}{4}$$

which in turn reduces to the nonnegativity of

Inequality 1

There are $6! =24$ possible orderings of $a,b,c,d$, and cyclic symmetry reduces the number of orderings we need to check to 6. Let $a$ denote the minimum value, and check each of the six possible orderings of $b,c,d$ in turn. For instance, taking $a\leq b\leq c\leq d$, set $b=a+u,c=a+u+v,d=a+u+v+w$, and expand—yielding a polynomial with over 600 lines! But checking it, we find every term has a positive coefficient, which completes the proof for this case. Checking the remaining cases, we find that only in the two cases $a\leq c\leq d\leq b$ and $a\leq c\leq b\leq d$ do negative terms appear, namely

$$3248 d^{17} u^3+ 1936 d^{17} u w^2- 1360 d^{17} u^2 w$$

and

$$- 192 d^{18} u w +224 d^{18} w^2+224 d^{18} u^2$$

and the nonnegativity of these two terms is obvious.

Closing Remarks

What this post offers is a form of "machine proof": using software to tirelessly carry out the polynomial expansions, and completing the proof either by directly checking the positivity of the coefficients or by reducing the problem to some simple sub-inequalities. What's surprising is that this technique turns out to be somewhat less capable when the inequality is required to hold over all real numbers, rather than being restricted to nonnegative reals—it needs further transformation before it can be applied. For example, to prove the Vasile inequality $(a^2+b^2+c^2)^2\geq 3(a^3 b+b^3 c+c^3 a)$, which holds for all real values of $a,b,c$, even if we restrict ourselves to nonnegative reals, the technique above cannot directly complete the proof in one shot; further transformation is needed.

Finally, I should explain why this post emphasizes "homogeneous" inequalities. In fact, homogeneous inequalities are the ones that carry genuine physical meaning: homogeneity means the "dimensions" on both sides are equal, which is exactly what I meant earlier by "physical proof." If an inequality is non-homogeneous, equality generally holds at some specific point rather than simply at $a=b=c$, which tends to increase the difficulty. Of course, as I've already mentioned, the applications of difference substitution are actually quite broad, and with suitable extensions it can be used to prove many non-homogeneous inequalities as well—but that lies beyond the scope of this post. Interested readers may want to look into the relevant papers or books first; perhaps we'll come back to this topic another time.

References

Methods for Proving Elementary Inequalities, edited by Han Jingjun
Machine Proof and Automated Discovery of Inequalities, by Yang Lu and Xia Bican