The following inequality is derived from this difficult olympiad problem.
Suppose $a,b,c$ are three positive real numbers such that $abc = 8$, show that
$$\frac{1}{\sqrt{a + 1}} + \frac{1}{\sqrt{b + 1}} + \frac{1}{\sqrt{c + 1}} < 2$$
My idea: Note that $\sqrt{x}$ is a concave function on $(0,\infty)$. Let $x,y,z,p,q,r$ be any positive real numbers, then according to weighted Jensen inequality we have
$$\begin{aligned}\sqrt{x} + \sqrt{y} + \sqrt{z} &= \frac{\sqrt{p^2x}}{p} + \frac{\sqrt{q^2y}}{q} + \frac{\sqrt{r^2z}}{r}\\&\leq\sqrt{\left(\frac{1}{p} + \frac{1}{q} + \frac{1}{r}\right)(px + qy + rz)}\end{aligned}$$
Let $x = a,y = b,z = c = \frac{8}{ab}$. If we can find appropriate weights $p,q,r$ such that
$$\left(\frac{1}{p} + \frac{1}{q} + \frac{1}{r}\right)(px + qy + rz) < 4$$
then we are done.
Now if I ask Mathematica
Reduce[ForAll[a, a > 0, ForAll[b, b > 0, Exists[{p, q, r}, p > 0 && q > 0 && r > 0 && (1/p + 1/q + 1/r) (p/(1 + a) + q/(1 + b) + r/(1 + 8/(a b))) < 4]]]]
Mathematica returns True in less than 2 seconds(!!). However, it provides no more details other than a truth value.
If I ask instead
Reduce[ForAll[a, a > 0, ForAll[b, b > 0, Exists[{p, q, r}, p > 0 && q > 0 && r > 0 && (1/p + 1/q + 1/r) (p/(1 + a) + q/(1 + b) + r/(1 + 8/(a b))) < m]]], m]
Mathematical returns m >= 4, although using much longer time.
Which algorithm does Mathematica use to verify the proposition? It is certainly not cylindrical algebra, for CylindricalDecomposition takes much much longer.
Can we find simple expressions for $p,q,r$ that would complete the proof?
Update: I have found a way to carry out quantifier elimination by hand. Therefore the first part of this problem is solved.
Best Answer
The Contradiction method works!
Let $\frac{1}{\sqrt{a+1}}=p,$ $\frac{1}{\sqrt{b+1}}=q$ and $\frac{1}{\sqrt{c+1}}=r.$
Thus, $\{p,q,r\}\subset(0,1),$ $\frac{(1-p^2)(1-q^2)(1-r^2)}{p^2q^2r^2}=8$ and we need to prove that: $$p+q+r<2.$$ Indeed, let $p+q+r\geq2,$ $r=kr'$ such that $k>0$ and $p+q+r'=2$.
Thus, $$p+q+kr'\geq2=p+q+r',$$ which gives $k\geq1.$
Thus, $$8=\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{k^2r'^2}-1\right)\leq\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{r'^2}-1\right),$$ which is a contradiction because we'll prove now that $$8>\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{r'^2}-1\right).$$ Indeed, we need to prove that $$8p^2q^2r'^2>(1-p^2)(1-q^2)(1-r'^2)$$ or $$512p^2q^2r'^2>((p+q+r')^2-4p^2)((p+q+r')^2-4q^2)((p+q+r')^2-4r'^2)$$ or $$512p^2q^2r'^2>(3p+q+r')(3q+p+r')(3r'+p+q)(p+q-r')(p+r'-q)(q+r'-p).$$ Now, if $(p+q-r')(p+r'-q)(q+r'-p)\leq0$, so our inequality is true, which says that it's enough to prove it for $(p+q-r')(p+r'-q)(q+r'-p)>0$.
Also, if $p+q-r'<0$ and $p+r'-q<0,$ so $p<0$, which is a contradiction.
Thus, we can assume that $p+q-r'=z>0,$ $p+r'-q=y>0$ and $q+r'-p=x>0$, which gives
$p=\frac{y+z}{2},$ $q=\frac{x+z}{2},$ $r'=\frac{x+y}{2}$ and we need to prove that $$8(x+y)^2(x+z)^2(y+z)^2>xyz\prod_{cyc}(x+2y+2z),$$ which is obviously true after full expanding.
Done!
It's interesting that even the following is true.