Поиграл с Microsoft Z3 theorem prover (самоизоляция - время эксцентричных хобби).
Прикольная штука: примерно как Wolfram Alpha, только можно подключать в свой собственный код в питоне. Можно сформулировать любую задачу как набор ограничений в логике первого порядка и попросить Z3 символьно найти решение.
В первой ячейке он решает уравнения, от кубических до 6й степени.
Во второй – доказывает неравенство Коши.
В третьей просто хрень, не справился.