Непростое неравенство

[g______d]

Побуду немного занудой и добавлю, что в принципе, проверка истинности системы полиномиальных неравенств с рациональными коэффициентами -- алгоритмически разрешимая задача.

https://en.wikipedia.org/wiki/Tarski–Seidenberg_theorem
https://en.wikipedia.org/wiki/Decidabil ... al_numbers

https://en.wikipedia.org/wiki/Cylindric ... omposition

(но время работы очень длинное).

Конкретно для данных неравенств, если бы стояла задача придумать computer assisted proof, я бы перенёс всё влево и искал минимум получившейся функции (там нужно будет сводить всё к октанту на сфере, поскольку функция однородная, таким образом, параметров на самом деле два). Сначала можно проверить внутренние точки области, для них обе производных должны обращаться в нуль, это два полиномиальных уравнения с двумя неизвестными, скорее всего с помощью базисов Грёбнера это сведётся к перебору конечного числа точек. Кроме этих точек, нужно ещё проверить границу области; но на границе это будет уже одномерная задача, там уже как-нибудь получится.

Интересно (хотя здесь наверное оффтоп), насколько GPU могут ускорить эти алгоритмы.

[g______d]

Решило! Минуты за две. Всё, больше не буду спамить.

In[1]:= FullSimplify[
 CylindricalDecomposition[{a^3/(13 a^2 + 5 b^2) + 
     b^3/(13 b^2 + 5 c^2) + c^3/(13 c^2 + 5 a^2) >= (a + b + c)/18, 
   a > 0, b > 0, c > 0}, {a, b, c}]]

Out[1]= a > 0 && b > 0 && c > 0

[nnosipov]

g______d в сообщении #1351514 писал(а):

Конкретно для данных неравенств, если бы стояла задача придумать computer assisted proof, я бы перенёс всё влево и искал минимум получившейся функции (там нужно будет сводить всё к октанту на сфере, поскольку функция однородная, таким образом, параметров на самом деле два). Сначала можно проверить внутренние точки области, для них обе производных должны обращаться в нуль, это два полиномиальных уравнения с двумя неизвестными, скорее всего с помощью базисов Грёбнера это сведётся к перебору конечного числа точек. Кроме этих точек, нужно ещё проверить границу области; но на границе это будет уже одномерная задача, там уже как-нибудь получится.

Я тоже так думал, пока не попробовал реализовать этот план на каком-нибудь неочевидном примере. На самом деле, может возникнуть куча дополнительных технических проблем с непредсказуемым результатом.

А вот то, что

CylindricalDecomposition

работает, и за очень разумное время --- это уже интересно. Другое дело, мы опять, скорее всего, не узнаем, насколько этим доказательствам можно доверять (я имею в виду Mathematica).

[g______d]

nnosipov в сообщении #1390648 писал(а):

Другое дело, мы опять, скорее всего, не узнаем, насколько этим доказательствам можно доверять (я имею в виду Mathematica).

Ну, это далеко не новый алгоритм, и он много где реализован. Вот нашёл обзор с большим количеством ссылок (в том числе и на программы с открытым кодом).

https://arxiv.org/pdf/1504.06484.pdf

Я так понимаю, что вариациями на его тему активно пользуются при компьютерной формализации доказательств.

[nnosipov]

g______d в сообщении #1390652 писал(а):

Вот нашёл обзор с большим количеством ссылок

Да, спасибо. Авторы известны, особенно первый.

[kotenok gav]

Есть еще такая книга, посвященная как раз таким доказательствам, очень хорошая. A=B называется, вроде.

[g______d]

Она в основном про комбинаторные тождества, судя по всему. Это другое.

[kotenok gav]

Далеко нет. Она в основном про нахождение суммы гипергеометрических функций. Возможно, там и для неравенств что-нибудь найдется.

[g______d]

kotenok gav в сообщении #1390834 писал(а):

Возможно, там и для неравенств что-нибудь найдется.

Если не открывать книгу -- то возможно.