ИИ использовали для проверки самого сложного на сегодняшний день математического доказательства

[teleomoon]

Было бы интересно проверить современными нейросетями доказательство abc-гипотезы от Синъити Мотидзуки.

[si_12345]

Да вот только незадача: Мотидзуки разработал для этого новый математический аппарат, который никто не понимает
Я думаю, что уже этот аппарат скормили ИИ, но пока тишина ...

[Seraphimt]

Зачем, если даже кожаные мешки давно нашли там ошибки?

[domix32]

Проблема в том что половину тех теорем, что там добавляется пока нельзя формализовать в робото-понятном формате. То бишь его нельзя записать в терминах Coq/Rocq/Lean/Agda или ещё какого-нибудь theorem proof assistant. По тому же принципу пока не формализован и геометрический Лэнглэндс, который точно работает - пока нет таких языков которые могли бы работать на уровне теории категорий в том виде в каком с ним работают на краю современной математики. Аналогичная проблема с гомологиями-когомологиями.

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

[PlextorTI]

Вся задача ии тут была простая, если проще переводчик с человека на машинный на языке Lean. Ни чего особенного тут не произошло. Далее этот перевод проверил верификатор.