lean_workbook_plus_32707

Let $a,b,c$ be positive. Then $(a^3+2)(b^3+2)(c^3+2)\le (a^3+b^3+c^3+6)^3/27.\ (1)$ We will show that the function $f(a,b,c)=(a^3+b^3+c^3+6)^3-27(872+16abc)\ (2)$ has a maximum of zero under the condition $a^2+b^2+c^2=12. \ (3)$