<s>[INST] Minimize $|a-1|^3+|b-1|^3$ with constant product $ab=s$ Let $0<s$, and define 
$$ F(s):=\min_{a,b \in \mathbb{R}^+,ab=s} \left(|a-1|^3+|b-1|^3\right). $$
I would like to find proofs for the claim
$$
F(s)=\begin{cases}
1 - 3 s - 2s^{3/2}=F\big(a(s),b(s)\big), &\text{ if } 0<s\le1/9, \\
2 + 6 s - 2(3 + s)s^{1/2}=F(\sqrt s,\sqrt s) &\text{ if } 1/9\le s<1,
\end{cases}
$$
where $a(s),b(s)$ are uniquely defined by the equation $a+b=1-\sqrt{s},ab=s$.
(Actually I am more interested in the exact value of $F(s)$, and less in the minima points themselves, but I thought that this additional information might be helpful to find other proofs as well). 

I have a proof which I present below, but I wonder if there is an easier way to prove this. 

Also, is there a math software that can solve such a problem? (I am rather ignorant on that stuff, unfortunately).
Edit:
I think that maybe one can prove this without differentiation, but I am not sure. The idea is to rewrite the symmetric polynomial $(a-1)^3+(b-1)^3$, as a polynomial in $a+b,ab$, and proceed from there, but I am not sure it really works.
My proof:
First, suppose that $s \le 1$. Then the minimum is obtained at a point $(a,b)$ where both $a,b$ are not greater than $1$. Indeed, if $a>1$ (and so $b <s \le 1$), we can replace $a$ by $1$ and $b$ by $s$ to get the same product, but now both numbers are closer to $1$ then before. In fact, a symmetric argument shows that if $s \ge 1$, then both $a,b \ge 1$.
In any case, the signs of $a-1,b-1$ are identical.
Expressing the constraint as $g(a,b)=ab-s=0$, and using Lagrange's multipliers, there exist a $\lambda$ such that
$$
(a-1)^2=\lambda b, (b-1)^2=\lambda a.
\tag{1}$$
(Here we used the assumption the fact that the signs of $a-1,b-1$ are identical).
Subtracting these equations, we get
$$
(a-b)(a+b-2)=-\lambda(a-b).
$$
So, one candidate is $a=b=\sqrt{s}$. If $a \neq b$, then 
$$
a+b=2-\lambda, ab =s \tag{2}.
$$
Thus, $a,b$ are the solutions of the quadratic 
$$ x^2+(\lambda-2)x+s=0$$ 
Say that $a \le b$. Then
$$ a=\frac{2-\lambda-\sqrt{c}}{2}, b=\frac{2-\lambda+\sqrt{c}}{2}, \, \, \, \text{where } \, \, c=(2-\lambda)^2-4s.$$
Plugging this into $(a-1)^2=\lambda b$ from equation $(1)$, we get
$$
(\lambda+\sqrt c)^2=\lambda (4-2\lambda+2\sqrt c),
$$
which simplifies into
$$ 3\lambda^2-4\lambda=-c=4s-(2-\lambda)^2.$$
Further simplification gives
$$ (\lambda-1)^2=s \Rightarrow 1-\lambda=\pm \sqrt s.$$
Thus, by equation $(2)$, $a+b=1\pm \sqrt s$. 
Comment: We can immediately see that this cannot happen when $s>1$. Applying the AM-GM inequality for $a,b$ implies that 
$$ a+b=1+\sqrt s \Rightarrow s \le 1, \,\,\,a+b=1-\sqrt s \Rightarrow  s \le \frac{1}{9}$$
Now, if $a+b=1 + \sqrt s$, the it is easy to deduce that $b \ge 1$. (recall we assumed before that $a \le b$). As commented at the beginning, the optimum point must be obtained where $a,b$ are both not greater than $1$. So, the only possible option is $b=1$, and then $a=\sqrt s$, which implies $s=ab=\sqrt s$ so $s=1$ and $F(1)=0$, $a=b=1$.
Thus, we are left with the option $a+b=1-\sqrt{s}$.
Solving explicitly the quadratic given by $a+b=1-\sqrt{s},ab=s$, we get explicit expressions $a(s),b(s)$. Then direct calculation gives
$$ F\big(a(s),b(s)\big)=1 - 3 s - 2s^{3/2}.$$
The quadratic for $a(s),b(s)$ is 
$$ x^2-(1-\sqrt s)x+s=0. \tag{3}$$
It has real solutions exactly when $(1-\sqrt s)^2 \ge 4s$, or (since $s>0$), $\sqrt s \le \frac{1}{3}$. (Equivalently, this can be seen from the AM-GM inequality for $a,b$ as above.)
Now,
$F(\sqrt s,\sqrt s)=2 + 6 s - 2(3 + s)s^{1/2}$, and all is left to do is to verify that 
$$ F(a(s),b(s)) \le F(\sqrt s,\sqrt s),$$ in the regime $s \le \frac{1}{9}$, where $a(s),b(s)$ exist, as solutions to the quadratic $(3)$.
Direct computation shows that
$$ F(\sqrt s,\sqrt s)-F(a(s),b(s))=(1-3\sqrt s)^2 \ge 0$$
(and equality happens only at $s=\frac{1}{9}$).
This finishes the proof.
 [/INST] Since you have established that the signs of $a - 1$ and $b - 1$ are identical, one approach would be to find the extrema of $(a - 1)^3 + (b-1)^3$ and then remove those where $a - 1$ and $b - 1$ are of opposite signs.
Plugging in $b = {s \over a}$ directly, you are finding an extremum of the expression
$$f(a) = (a - 1)^3 + ({s \over a} - 1)^3$$
So the goal becomes to find a $a$ for which $f'(a) = 0$. If you do the algebra, $f'(a) = 0$ at some $a$ satisfying
$$(a - \sqrt{s})(a^2 + (\sqrt{s} - 1)a + s) = 0$$
So you have two possibilities, either $a = b = \sqrt{s}$, or $a$ and $b$ are the two roots of the quadratic equation $x^2 + (\sqrt{s} - 1)x + s = 0$. You can then plug these two possibilities into the expression $(a - 1)^3 + (b - 1)^3 $ to compare the two situations.
While this may look unpleasant to do, since $(a - 1)^3 + (b - 1)^3$ is a symmetric polynomial $(a^3 + b^3) - 3(a^2 + b^2) + 3(a + b) - 1$, you will end out getting a polynomial in $\sqrt{s}$ using $a + b = 1 - \sqrt{s}$ and $ab = s$. You seem to have already computed it to be $1 - 3s - 2s^{3 \over 2}$.
</s>