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{1t^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$.

$\begingroup$ Thanks. From Lagrange Multiplier method, one can see that $a,b,c,d$ can take at most two values. Then one can try setups as you display here. But is there any elementary way to tackle this type of problems? $\endgroup$ – Haoran Chen Jun 7 '18 at 10:32

$\begingroup$ What do you mean by "elementary"? The first step in my process was to try some randomly generated cases; I'd say that's pretty elementary (and certainly much faster than theoretical analysis as in Iosif Pinelis's answer). When the function is not too complicated, and the number of variables is not too large, random search is quite reliable for suggesting the right answer, which you can then try to prove rigorously. $\endgroup$ – Neil Strickland Jun 7 '18 at 10:42

$\begingroup$ I agree on your process and I tried variational method which gives the maximum at $(a,a,a,d)$ or something like that. I was thinking any method without using calculus. $\endgroup$ – Haoran Chen Jun 7 '18 at 11:28
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 semialgebraic sets, and Fewnomials. Much of this goes back to Tarski, A Decision Method for Elementary Algebra and Geometry.

$\begingroup$ Can you give me an elementary book or any resources that tells the connection between inequalities and algebraic geometry, thanks! $\endgroup$ – Haoran Chen Jun 7 '18 at 10:36

$\begingroup$ @HaoranChen : I have now provided references to a few relevant sources on real algebraic geometry. $\endgroup$ – Iosif Pinelis Jun 7 '18 at 13:28
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 $$(x1)^2(4x^{14}+8x^{13}+12x^{12}+28x^{11}+44x^{10}+60x^915x^854x^769x^684x^545x^4+30x^3+105x^2+180x+36)\geq0,$$ which is obvious by AMGM.
By this method you can create infinitely many inequalities.

1
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 TarskiSeidenberg 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 MarieFrançoise Roy.