For the second one - is there specific software for proving inequalities or you use software just for calculations?
Можно сделать следующее:
1. заменить все переменные на их кубы;
2. превратить неравенство в однородное;
3. поскольку неравенство циклическое, то можно считать, что

,

и

.
Подставляем и с помощью компьютера раскрываем скобки, приводим подобные члены.
Получается многочлен от

, у которого все коэффициенты (многочлены от

и

) неотрицательны.
Метод дебильный (не зря он называется Buffalo Way), но очень эфективный и если степень неравенства не очень высокая, его можно успешно применять и на олимпиаде без всякого компьютера.
Вот симпатичное неравенство от четырёх переменных на этот метод:
Докажите, что для всех действительных

,

,

и

верно следующее неравенство:

Можно, конечно, попытаться доказать его и по-другому.