# Proving large inequality in 6 variables

I have arrived at a very large inequality in 6 variables that I would like to prove is true. The command I have tried is the following:

Reduce[(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6)^2*
x^6 + (-2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 +
a^3/6))*x^5*
y + (-2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 +
a^3/6))*x^5*z + (-2*a^2*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*
x^5 + (((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)^2 -
2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*
x^4*y^2 + (2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*((a*c)/2 -
c*(a/2 - a^2/2) + (a^2*c)/2) - 4*a*b*c*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*
x^4*y*z + (2*a^2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) -
4*a*b*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*x^4*
y + (((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)^2 -
2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*
x^4*z^2 + (2*a^2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) -
4*a*c*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6))*x^4*
z + (a^4 - 2*a*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) - a*(a^3/6 - a^2/2 + a/3))*
x^4 + (2*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6)*(b/3 + b*(b/2 - b^2/2) - b^2/2 +
b^3/6) + 2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*((a*b)/2 -
a*(b/2 - b^2/2) + (a*b^2)/2))*x^3*
y^3 + (2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*((a*c)/2 -
c*(a/2 - a^2/2) + (a^2*c)/2) -
2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 +
a^3/6) + 4*a*b*c*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2))*x^3*y^2*
z + (2*a^2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) -
2*b^2*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) +
4*a*b*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2))*x^3*
y^2 + (2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*((a*c)/2 -
a*(c/2 - c^2/2) + (a*c^2)/2) -
2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2)*(a/3 + a*(a/2 - a^2/2) - a^2/2 +
a^3/6) + 4*a*b*c*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2))*x^3*y*
z^2 + (4*a*c*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) +
4*a*b*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) -
4*b*c*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) + 4*a^3*b*c)*x^3*y*
z + (4*a^3*b - 2*b*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) -
b*(a^3/6 - a^2/2 + a/3) + a*((a*b)/2 - (a^2*b)/2) +
2*a*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2))*x^3*
y + (2*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6) + 2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*((a*c)/2 -
a*(c/2 - c^2/2) + (a*c^2)/2))*x^3*
z^3 + (2*a^2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) -
2*c^2*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) +
4*a*c*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2))*x^3*
z^2 + (4*a^3*c - 2*c*(a/3 + a*(a/2 - a^2/2) - a^2/2 + a^3/6) -
c*(a^3/6 - a^2/2 + a/3) + a*((a*c)/2 - (a^2*c)/2) +
2*a*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2))*x^3*
z + (a*(a/2 - a^2/2) - a/3 + a^2/2 + (11*a^3)/6)*
x^3 + (((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)^2 -
2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*
x^2*y^4 + (2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*((b*c)/2 -
c*(b/2 - b^2/2) + (b^2*c)/2) -
2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 +
b^3/6) + 4*a*b*c*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2))*x^2*y^3*
z + (2*b^2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) -
2*a^2*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) +
4*a*b*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2))*x^2*
y^3 + (2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*((a*c)/2 -
a*(c/2 - c^2/2) + (a*c^2)/2) +
2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*((b*c)/2 -
b*(c/2 - c^2/2) + (b*c^2)/2) +
2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*((b*c)/2 -
c*(b/2 - b^2/2) + (b^2*c)/2) + 4*a^2*b^2*c^2)*x^2*y^2*
z^2 + (2*b^2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) +
2*a^2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) +
4*a*c*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) +
4*b*c*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) + 8*a^2*b^2*c)*x^2*y^2*
z + (a*((a*b)/2 - (a*b^2)/2) + b*((a*b)/2 - (a^2*b)/2) +
2*a*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) +
2*b*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) + 6*a^2*b^2)*x^2*
y^2 + (2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*((b*c)/2 -
b*(c/2 - c^2/2) + (b*c^2)/2) -
2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6) + 4*a*b*c*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2))*x^2*y*
z^3 + (2*c^2*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) +
2*a^2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) +
4*a*b*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) +
4*b*c*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) + 8*a^2*b*c^2)*x^2*y*
z^2 + (c*((a*b)/2 - (a^2*b)/2) + b*((a*c)/2 - (a^2*c)/2) +
2*c*((a*b)/2 - b*(a/2 - a^2/2) + (a^2*b)/2) +
2*b*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) + 15*a^2*b*c)*x^2*y*
z + (b*(a/2 - a^2/2) + (a*b)/2 + (9*a^2*b)/2)*x^2*
y + (((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)^2 -
2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*
x^2*z^4 + (2*c^2*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) -
2*a^2*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) +
4*a*c*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2))*x^2*
z^3 + (a*((a*c)/2 - (a*c^2)/2) + c*((a*c)/2 - (a^2*c)/2) +
2*a*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) +
2*c*((a*c)/2 - c*(a/2 - a^2/2) + (a^2*c)/2) + 6*a^2*c^2)*x^2*
z^2 + (c*(a/2 - a^2/2) + (a*c)/2 + (9*a^2*c)/2)*x^2*z + (a^2/2 + a/2)*
x^2 + (-2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 +
b^3/6))*x*y^5 + (2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*((b*c)/2 -
c*(b/2 - b^2/2) + (b^2*c)/2) - 4*a*b*c*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*
x*y^4*z + (2*b^2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) -
4*a*b*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*x*
y^4 + (2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*((b*c)/2 -
b*(c/2 - c^2/2) + (b*c^2)/2) -
2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 +
b^3/6) + 4*a*b*c*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2))*x*y^3*
z^2 + (4*b*c*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) +
4*a*b*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) -
4*a*c*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) + 4*a*b^3*c)*x*y^3*
z + (4*a*b^3 - 2*a*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) -
a*(b^3/6 - b^2/2 + b/3) + b*((a*b)/2 - (a*b^2)/2) +
2*b*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2))*x*
y^3 + (2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)*((b*c)/2 -
c*(b/2 - b^2/2) + (b^2*c)/2) -
2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6) + 4*a*b*c*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2))*x*y^2*
z^3 + (2*c^2*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) +
2*b^2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) +
4*a*b*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) +
4*a*c*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) + 8*a*b^2*c^2)*x*y^2*
z^2 + (c*((a*b)/2 - (a*b^2)/2) + a*((b*c)/2 - (b^2*c)/2) +
2*c*((a*b)/2 - a*(b/2 - b^2/2) + (a*b^2)/2) +
2*a*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) + 15*a*b^2*c)*x*y^2*
z + (a*(b/2 - b^2/2) + (a*b)/2 + (9*a*b^2)/2)*x*
y^2 + (2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)*((b*c)/2 -
b*(c/2 - c^2/2) + (b*c^2)/2) - 4*a*b*c*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*
x*y*z^4 + (4*b*c*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) +
4*a*c*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) -
4*a*b*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) + 4*a*b*c^3)*x*y*
z^3 + (b*((a*c)/2 - (a*c^2)/2) + a*((b*c)/2 - (b*c^2)/2) +
2*b*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) +
2*a*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) + 15*a*b*c^2)*x*y*z^2 + (8*a*b*c)*x*y*
z + (a*b)*x*
y + (-2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6))*x*
z^5 + (2*c^2*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2) -
4*a*c*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*x*
z^4 + (4*a*c^3 - 2*a*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) -
a*(c^3/6 - c^2/2 + c/3) + c*((a*c)/2 - (a*c^2)/2) +
2*c*((a*c)/2 - a*(c/2 - c^2/2) + (a*c^2)/2))*x*
z^3 + (a*(c/2 - c^2/2) + (a*c)/2 + (9*a*c^2)/2)*x*z^2 + (a*c)*x*
z + (b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6)^2*
y^6 + (-2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 +
b^3/6))*y^5*z + (-2*b^2*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*
y^5 + (((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2)^2 -
2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2)*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*
y^4*z^2 + (2*b^2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) -
4*b*c*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6))*y^4*
z + (b^4 - 2*b*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) - b*(b^3/6 - b^2/2 + b/3))*
y^4 + (2*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6) +
2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2)*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2))*
y^3*z^3 + (2*b^2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) -
2*c^2*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) +
4*b*c*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2))*y^3*
z^2 + (4*b^3*c - 2*c*(b/3 + b*(b/2 - b^2/2) - b^2/2 + b^3/6) -
c*(b^3/6 - b^2/2 + b/3) + b*((b*c)/2 - (b^2*c)/2) +
2*b*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2))*y^3*
z + (b*(b/2 - b^2/2) - b/3 + b^2/2 + (11*b^3)/6)*
y^3 + (((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2)^2 -
2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*
y^2*z^4 + (2*c^2*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) -
2*b^2*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) +
4*b*c*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2))*y^2*
z^3 + (b*((b*c)/2 - (b*c^2)/2) + c*((b*c)/2 - (b^2*c)/2) +
2*b*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) +
2*c*((b*c)/2 - c*(b/2 - b^2/2) + (b^2*c)/2) + 6*b^2*c^2)*y^2*
z^2 + (c*(b/2 - b^2/2) + (b*c)/2 + (9*b^2*c)/2)*y^2*z + (b^2/2 + b/2)*
y^2 + (-2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2)*(c/3 + c*(c/2 - c^2/2) - c^2/2 +
c^3/6))*y*z^5 + (2*c^2*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2) -
4*b*c*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*y*
z^4 + (4*b*c^3 - 2*b*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) -
b*(c^3/6 - c^2/2 + c/3) + c*((b*c)/2 - (b*c^2)/2) +
2*c*((b*c)/2 - b*(c/2 - c^2/2) + (b*c^2)/2))*y*
z^3 + (b*(c/2 - c^2/2) + (b*c)/2 + (9*b*c^2)/2)*y*z^2 + (b*c)*y*
z + (c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6)^2*
z^6 + (-2*c^2*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6))*
z^5 + (c^4 - 2*c*(c/3 + c*(c/2 - c^2/2) - c^2/2 + c^3/6) - c*(c^3/6 - c^2/2 + c/3))*
z^4 + (c*(c/2 - c^2/2) - c/3 + c^2/2 + (11*c^3)/6)*z^3 + (c^2/2 + c/2)*z^2 <
0 && {x, y, z} \[Element] Reals && {a, b, c} \[Element] Integers && a >= 0 && b >= 0 &&
c >= 0, {x, y, z}]


My anticipation is for this query to output 'false' i.e that the monstrous expression is positive. The above command does not seem to terminate. I'm a complete new beginner to Mathematica. My question is therefore:

Can I hope to answer this question in Mathematica, or am I being completely unrealistic?

If it can be answered, is there a better way of formulating this query so that it terminates?

### Edit

I should also mention that the command terminates with 'false' if I restrict a, b, c to some specific positive integers (though there seems to be significant slowdown the larger the integers get). I moreover suspect that the expression is positive even with a, b, c relaxed to the positive reals (or even all reals) if that benefits the solver. If it helps the inequality is obtained in more human readable terms as follows:

p1 := a*x+b*y+c*z
p2 := a*x^2+b*y^2+c*z^2
p3 := a*x^3+b*y^3+c*z^3
e1 := p1
e2 := (1/2)*(p1^2 - p2)
e3 := (1/6)*p1^3 - (1/2)*p2*p1 + (1/3)*p3
func := (e1^2 + e1*e2 + e1 - e3)^2 - e2 - e3 - e1*e2 - e1*e3
Reduce[func < 0 && a >= 0 && b >= 0 && c >= 0, {a, b, c, x, y, z}]


As per comments the inequality has been disproved when a,b,c are relaxed to positive reals. Therefore one must evaluate the statement below (in whichever form)

Reduce[func < 0 && {a,b,c} \[Element] Integers && a >= 0 && b >= 0 && c >= 0, {a, b, c, x, y, z}]


The statement seems to hold for all positive integers a,b,c such that a+b+c <= 10 as the following snippet shows

p1[a_, b_, c_] := a*x + b*y + c*z
p2[a_, b_, c_] := a*x^2 + b*y^2 + c*z^2
p3[a_, b_, c_] := a*x^3 + b*y^3 + c*z^3
e1[a_, b_, c_] := p1[a,b,c]
e2[a_, b_, c_] := (1/2)*(p1[a,b,c]^2 - p2[a,b,c])
e3[a_, b_, c_] := (1/6)*p1[a,b,c]^3 - (1/2)*p2[a,b,c]*p1[a,b,c] + (1/3)*p3[a,b,c]
discriminant[a_, b_, c_] := (e1[a,b,c]^2 + e1[a,b,c]*e2[a,b,c] + e1[a,b,c] - e3[a,b,c])^2 - e2[a,b,c] - e3[a,b,c] - e1[a,b,c]*e2[a,b,c] - e1[a,b,c]*e3[a,b,c]
isDiscriminantPositive[n_] := Not[Or @@ Function[p, Reduce[discriminant[p[[1]], p[[2]], p[[3]]] < 0, {x,y,z}]]/@(Function[l,PadRight[l,{3}]]/@IntegerPartitions[n,3])]


In[1]:= isDiscriminantPositive[5]

Out[1]= True

In[2]:= isDiscriminantPositive[6]

Out[2]= True

In[3]:= isDiscriminantPositive[7]

Out[3]= True

In[4]:= isDiscriminantPositive[8]

Out[4]= True

In[5]:= isDiscriminantPositive[9]

Out[5]= True

In[6]:= isDiscriminantPositive[10]

Out[6]= True

• Welcome to Mathematica.SE! I suggest that: 1) You take the introductory Tour now! 2) When you see good questions and answers, vote them up by clicking the gray triangles, because the credibility of the system is based on the reputation gained by users sharing their knowledge. Also, please remember to accept the answer, if any, that solves your problem, by clicking the checkmark sign! 3) As you receive help, try to give it too, by answering questions in your area of expertise. – bbgodfrey Jan 24 '15 at 7:37
• My first reaction: i.stack.imgur.com/vhsuV.jpg -- fortunately I probably don't know what I'm talking about in this particular case. – Mr.Wizard Jan 24 '15 at 7:38
• The first thing I would do is to evaluate this expression for, say, a million points. If any are negative, then you do not need to waste time trying to prove that the expression is positive definite. If they are all positive, perhaps you can analyze the expressions that went into obtaining this expression, because it seems unlikely that you Reduce will be able to show that the expression is positive definite in a reasonable amount of time, or even at all. (A successful proof would cast the expression into a sum of squares.) – bbgodfrey Jan 24 '15 at 7:51
• I've actually tried sampling precisely 1M points in order to look for counterexamples, but none was found which is what leads me to believe it is positive. The expression has been expanded from a certain expression in elementary symmetric polynomials, so it is symmetric (but not homogeneous). – NewUser Jan 24 '15 at 7:55
• The term actually has negative solutions, e.g. for: {a,b,c,x,y,z}={579034,146345,766709,461054.,884854., -517892.} and (of course) others. – Jinxed Jan 24 '15 at 10:20