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

[teleomoon]

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

[si_12345]

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

[Seraphimt]

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

[domix32]

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

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

[domix32]

Сглазил. Антропик таки натравил иишницу и оно вроде как корректно. 13 млн строчек кода на Lean.

[Balling]

Да, оно корректно. Вот сайт. https://tianyipeng.github.io/fermats-last-theorem/

И там уже 246 улучшили до 212, а потом до 186.

[domix32]

Да, оно корректно.

Если вы не занимались подобной математикой, то каким образом вы можете это утверждать? Даже тот кто занимался формализацией FLT не убеждён на все 100%. Тут на днях гипотезу Коллатца полдня считали подтвержденной, пока не выяснилось, что в ядре Lean затесался косяк в обработке завтипов. И там размеры пруфа были довольно скромные. А тут 13 лямов строчек - втрое больше чем стандартная библиотека для Lean - шансы найти баг в компиляторе не нулевой.

[Balling]

“Тут на днях гипотезу Коллатца полдня считали подтвержденной, пока не выяснилось, что в ядре Lean затесался косяк в обработке завтипов.”

Никто не считал так, это был баг в Lean. И там не такое, что встречается в математичисих статьях. Его уже исправили. Как и новые баги в версии 34-rc1 https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/

[domix32]

Ну, как минимум необходимо повторно запускаться на этом rc1 с фиксами, репа FLT говорит о 4.33.1, который ещё с багами.

[PlextorTI]

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

[Balling]

Axiom Math: «Эта теорема в настоящее время представляет собой предел человеческих знаний о простых числах».

Уже не является. Вот 240 уже, а не 246. https://arxiv.org/abs/2608.31126