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.

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$.
