Algebraic inequalities on different means If $a^2+b^2+c^2+d^2=1$ in which $a,b,c,d>0$, prove or disprove
\begin{equation*}
\begin{aligned}
(a+b+c+d)^8&\geq 2^{12}abcd;\\
a+b+c+d+\frac{1}{2(abcd)^{1/4}}&\geq 3.
\end{aligned}
\end{equation*}
Can you tell any general algorithm for this type of problems? Thanks.
 A: Put 
\begin{align*}
 f(a,b,c,d) &= \frac{(a+b+c+d)^8}{2^{12}abcd} \\
 g(a,b,c,d) &= \frac{a+b+c+d}{3} + \frac{1}{6(abcd^{1/4})}
\end{align*}
so the conjecture is that $f,g\geq 1$.  I used Maple to search randomly for places where $f$ is as small as possible, then used Maple's fsolve() to find a local minimimum of $f$ numerically, then used Maple's identify() function to see whether there was any simple closed expression for the local minimum.  I found that
$$ f\left(\frac{1}{2\sqrt{3}},\frac{1}{2\sqrt{3}},\frac{1}{2\sqrt{3}},\frac{3}{2\sqrt{3}}\right) = \frac{3^5}{2^8} = \frac{243}{256} < 1;
$$
this is a local minimum and probably a global minimum.
Numerical methods also indicate that $g$ has a local minimum at a point of the form $(a,a,a,d)$.  This must have $3a^2+d^2=1$, so for some $t\in(0,1)$ we have
\begin{align*}
 a &= \frac{1}{\sqrt{3}} \frac{1-t^2}{1+t^2} \\
 d &= \frac{2t}{1+t^2}.
\end{align*}
Define $G(t)=g(a,a,a,d)$, with $a$ and $d$ as above.  We find that for $t_0=2-\sqrt{3}$ we have $G(t_0)=1$ and $G'(t_0)=G''(t_0)=0$, so this is not a local minimum.  Instead, there is a local minimum at a point $t_1\simeq 0.3868865016$ which is algebraic of degree 21 over $\mathbb{Q}(\sqrt{3})$, with $G(t_1)\simeq 0.99970268716$.
A: These are problems of real algebraic geometry (I have added the corresponding tag) and as such can, at least in principle, be solved completely algorithmically. In Mathematica, such algorithms are implemented via Reduce[], FindInstance[], Maximize[], and other similar commands. However, solving such problems on a computer may take too much time and/or memory. 
In this case, it took several hours (I forgot to measure the execution time) to get the following results: 

and

Thus, for each of the two conjectured inequalities FindInstance[] found an instance when the inequality fails to hold. 
Relevant literature on real algebraic geometry includes the following items, among many other ones: Computer Algebra, Computational real algebraic geometry, Real algebraic and semi-algebraic sets, and Fewnomials. Much of this goes back to Tarski, A Decision Method for Elementary Algebra and Geometry. 
A: There is a general algorithm for this type of problems.
We can use the Vasc's EV Method: https://www.emis.de/journals/JIPAM/images/059_06_JIPAM/059_06.pdf
For example, your second inequality is wrong, but the following is true.

Let $a$, $b$, $c$ and $d$ be positive numbers such that $a^2+b^2+c^2+d^2=1$. Prove that:
  $$a+b+c+d+\frac{2}{3\sqrt[4]{abcd}}\geq\frac{10}{3}.$$

Indeed, let $a+b+c+d=constant.$
Thus, it's enough to prove our inequality for a maximal value of $abcd$, which  by Corollary 1.8(b) 
happens for equality case of three variables.
After homogenization we need to prove that
$$a+b+c+d+\frac{2(a^2+b^2+c^2+d^2)}{3\sqrt[4]{abcd}}\geq\frac{10}{3}\sqrt{a^2+b^2+c^2+d^2}.$$
Now, let $a=x^4$, where $x>0$ and $b=c=d=1$.
Thus, we need to prove that
$$x^4+3+\frac{2(x^8+3)}{3x}\geq\frac{10}{3}\sqrt{x^8+3}$$ or after squaring of the both sides
$$(x-1)^2(4x^{14}+8x^{13}+12x^{12}+28x^{11}+44x^{10}+60x^9-15x^8-54x^7-69x^6-84x^5-45x^4+30x^3+105x^2+180x+36)\geq0,$$ which is obvious by AM-GM.
By this method you can create infinitely many inequalities. 
A: Too long for a comment, but in fact, there is an algorithm to decide whether an arbitrary (finite) collection of inequalities has a real solution. This is called the Tarski-Seidenberg theorem. For a textbook proof of that theorem one can refer to Chapter 1 (especially Section 1.4) of the book Real Algebraic Geometry by Jacek Bochnak, Michel Coste and Marie-Françoise Roy.
