Happy Pi Day! If Euler wasn't so keen on complex numbers then instead of $e^{i\pi}+1=0$ he would certainly have declared $$\pi^3+1=2^5$$ as the most beautiful equation. (Both sides indeed equal $32.0$). We can easily give a formal proof of this identity with MOSEK. Note that we need to simultaneously prove two inequalities $$\sqrt[3]{31}\geq \pi\quad \mathrm{and}\quad \sqrt[5]{\pi^3+1}\geq 2.$$ In MOSEK we have the geometric mean cone of dimension $n+1$: $$\mathcal{GM}^{n+1}=\{(x_1,\ldots,x_n,t)~:~x\geq 0, (x_1\cdot\ldots\cdot x_n)^{1/n}\geq |t|\},$$ so all we need to check is the feasibility of the conic problem $$(31,1,1,\pi)\in\mathcal{GM}^4,\quad (\pi^3+1,1,1,1,1,2)\in\mathcal{GM}^6.$$ This is straightforward with, for instance, Python Fusion:
M.constraint(Expr.constTerm([31, 1, 1, pi]),
Domain.inPGeoMeanCone())
M.constraint(Expr.constTerm([pi**3+1, 1, 1, 1, 1, 2]),
Domain.inPGeoMeanCone())
and voila! here is our proof:
Bonus question for the advanced user: which Mosek parameters do you have to modify to get this answer? Can you get away with only modifying one parameter by not too much? You can try to run it and find out yourself here.
