For $a^3+b^3+c^3=3$ prove that $a^4b+b^4c+c^4a\leq3$

Since $(a,b,c)$ is restricted to a compact set, it follows that $F_2 := a^4b +b^4 c + c^4 a$ has a maximal value, which must either be at an endpoint (i.e. one of $a,b,c$ is $0$, but these cases are easily eliminated) or at a point where the derivatives vanish.

Let $F_1 := a^3+b^3+c^3$. If we keep $c$ fixed and equate $F_1$ to $3$, then $b$ is a function of $a$, and we can use this to differentiate $F_2$ with respect to $a$. Equating that derivative to $0$ gives an equation. We can do the same with the roles of $a,b,c$ rotated and we get three equations:

$E = \{-a^6+4a^3b^3-4a^2b^3c+b^2c^4 = 0, 4a^3bc^2-4a^3c^3-a^2b^4+c^6 = 0, a^4c^2-4ab^2c^3-b^6+4b^3c^3 = 0\}$

To maximize $F_2$ under $F_1 = 3$, solve the equations $E \bigcup \{F_1 = 3\}$ (I need a computer for this step). These equations have 84 solutions. Most of them are complex. The only real solutions are $\{a,b,c\} = \{-0.26829, 0.80474, 1.3569\}$ and $\{a,b,c\}=1$. The only non-negative solution of $E \bigcup \{F_1 = 3\}$ is $a=b=c=1$. So that is where $F_2$ takes its maximum.

I have to ask: where did the problem come from, and was it formulated in a way that indicates that there should also be an answer that can be found with human-only computation? One way to reduce the computation would be to solve $E \bigcup \{F_1=3, F_2=3\}$ (only solution is $a=b=c=1$) (unlike my first method, it would be possible to produce a human-verifyable proof for this) and then consider derivatives at this point to show that this is a local maximum of $F_2$. That would produce a proof with computations short enough to be human-verifyable, though it still wouldn't be a nice proof.

The Buffalo Way works. However it is not nice.

Let me describe Michael Rozenberg's solution. We have \begin{align} \sum_{\mathrm{cyc}} a^4b &\le \frac{1}{3}\sum_{\mathrm{cyc}} (a^{9/2}b^{3/2} + a^{9/2}b^{3/2} + a^3)\\ &= \frac{2}{3} \sum_{\mathrm{cyc}} a^{9/2}b^{3/2} + \frac{1}{3} (a^3+b^3+c^3)\\ &\le \frac{2}{9} (a^3+b^3+c^3)^2 + \frac{1}{3} (a^3+b^3+c^3)\\ &= 3 \end{align} where we have used Vasc's inequality $(x^2+y^2+z^2)^2\ge 3(x^3y+y^3z+z^3x)$ to obtain $\sum_{\mathrm{cyc}} a^{9/2}b^{3/2} \le \frac{1}{3}(a^3+b^3+c^3)^2$.

This inequality can be used to prove the following inequality:

Let $x,y,z>0$ and $x^7+y^7+z^7=3$. Prove that $\frac{x^4}{y^3}+\frac{y^4}{z^3}+\frac{z^4}{x^3}\ge 3$.

Proof: Using AM-GM, we have $7\frac{x^4}{y^3} + 9 x^{28/3} y^{7/3} \ge 16 x^7$ which results in $$7 \sum_{\mathrm{cyc}} \frac{x^4}{y^3} + 9 \sum_{\mathrm{cyc}} x^{28/3} y^{7/3} \ge 16 (x^7+y^7+z^7). $$ It suffices to prove that $\sum_{\mathrm{cyc}} x^{28/3} y^{7/3} \le 3$. Let $a = x^{7/3}, \ b = y^{7/3}, \ c = z^{7/3}$. The condition becomes $a^3+b^3+c^3 = 3$. We need to prove that $a^4b+b^4c+c^4a \le 3$. We are done.