I've found this inequality, it seems cute:
$$\sqrt{2} + 2 \sqrt{3} + 2 \sqrt{5} + \sqrt{7} < 12$$
Note: It checks with a calculator. I am also interested in some methods that work for more general sum of radicals.
Thank you for your interest!
$\bf{Added:}$ I found this inequality by some random search. Note that all of the coefficients on LHS are positive, this can be an advantage. In the method of @heropup, one wants to check that a certain integer $N$ ( here $N=12$) is larger than a totally real algebraic number $\alpha$ that is larger than all the other conjugates $\alpha_j$. Say its minimal polynomial is $f(x)$. Then we need to show that $N>$ all of the roots of $f(x)$. Note that the roots of all derivatives of $f$ are also between the largest and the smallest of $\alpha_j$'s. The above inequality is equivalent to $f(N)$, $f'(N)$, $f''(N)$, $\ldots > 0$. With Taylor's formula, this is equivalent to: the polynomial $f(N+t)$ has all of the coefficients positive in $t$. This is an automated check that can be done instantly after we found $f(x)$.
This method does not work if $\alpha$ is not the largest ( or smallest) of all its conjugates. But there is a way to "make it the larges" using a transformation $x \mapsto 1/(a-x)$. I will leave out the details.
There was a previous question on this site about finding a general method for comparing arbitrary real algebraic numbers. That seems like a quite involved problem. It is easy to compare with $0$ a real algebraic number $\alpha$ with all its other conjugates non-real. The test is simple
$\alpha> 0$ if and only if $N(\alpha) > 0$, where $N(\cdot)$ is the norm. In particular this applies to cubic fields with discriminant $<0$. The general problem of comparing with $0$ an algebraic number $\alpha$ is simple if $\alpha$ is the $k$-th smallest ( or largest) root of an irreducible polynomial. Indeed, one needs to see how many positive/negative roots does the polynomial have , something that can be decided ( in principle). This is harder if one is given an expression involving several real algebraics. Even if we can find an equation whose root is the given expression, it could be harder to decide the order rank of the roots. So this seems like a difficult problem. But perhaps it is solved somewhere in the literature.
One other approach of @Parcly Taxel: simply gets rid of all the roots, little by little, something that I thought not possible just by counting. That is interesting! I am not fully convinced that it is so for an arbitrary number of roots as I was assured by Parcly… tempting to through another challenge to see how that works, what is the logic there…
Another approach, of @Luke Collins, and @Claude Leibovici uses the approximation of square roots with their convergents. It turns out that the convergents are easy to form, since the continued fractions are periodic ( and in this case, quite simple).
Summing up: some methods are ingenious and algebraic, other use some the minimal polynomial, other use continued fractions and convergents. Perhaps I should mention that there are other way to approximate roots. Parcly seems to prefer power series. I like Newton's method. Claude Leibovici might like Pade approximants too.
I've learned a lot from All the answers! Thank you very much to All the contributors!
Best Answer
Rewrite the LHS as $$\frac43\sqrt{1+\frac18}+4\sqrt{1-\frac14}+4\sqrt{1+\frac14}+\frac83\sqrt{1-\frac1{64}}$$ and use the binomial series to derive upper bounds for each term. For the series corresponding to $2\sqrt3$ and $\sqrt7$ every partial sum is an upper bound since all terms after the zeroth are negative. For the other two series only the partial sums up to odd-indexed terms (even number of terms total) form valid upper bounds since those series alternate and odd-indexed terms are positive.
Taking four terms (up to index $3$) for the first three series and just two (up to index $1$) for the $\sqrt7$ series yields an upper bound of $$\frac{8689}{2^{11}×3}+\frac{887}{2^8}+\frac{1145}{2^8}+\frac{127}{2^4×3}<12$$ where the denominators have been factorised to emphasise the relative ease of doing this by hand.