Comments 11
Было бы интересно проверить современными нейросетями доказательство abc-гипотезы от Синъити Мотидзуки.
Да вот только незадача: Мотидзуки разработал для этого новый математический аппарат, который никто не понимает
Я думаю, что уже этот аппарат скормили ИИ, но пока тишина ...
Зачем, если даже кожаные мешки давно нашли там ошибки?
Проблема в том что половину тех теорем, что там добавляется пока нельзя формализовать в робото-понятном формате. То бишь его нельзя записать в терминах Coq/Rocq/Lean/Agda или ещё какого-нибудь theorem proof assistant. По тому же принципу пока не формализован и геометрический Лэнглэндс, который точно работает - пока нет таких языков которые могли бы работать на уровне теории категорий в том виде в каком с ним работают на краю современной математики. Аналогичная проблема с гомологиями-когомологиями.
Подвижки в ту сторону есть, но пока не сказать чтобы сильно быстрые. Пока что самое близкое к краю - формализация последней теоремы ферма, которая все ещё в процессе на текущий момент.
Да, оно корректно. Вот сайт. https://tianyipeng.github.io/fermats-last-theorem/
И там уже 246 улучшили до 212, а потом до 186.
Да, оно корректно.
Если вы не занимались подобной математикой, то каким образом вы можете это утверждать? Даже тот кто занимался формализацией FLT не убеждён на все 100%. Тут на днях гипотезу Коллатца полдня считали подтвержденной, пока не выяснилось, что в ядре Lean затесался косяк в обработке завтипов. И там размеры пруфа были довольно скромные. А тут 13 лямов строчек - втрое больше чем стандартная библиотека для Lean - шансы найти баг в компиляторе не нулевой.
“Тут на днях гипотезу Коллатца полдня считали подтвержденной, пока не выяснилось, что в ядре Lean затесался косяк в обработке завтипов.”
Никто не считал так, это был баг в Lean. И там не такое, что встречается в математичисих статьях. Его уже исправили. Как и новые баги в версии 34-rc1 https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/
Вся задача ии тут была простая, если проще переводчик с человека на машинный на языке Lean. Ни чего особенного тут не произошло. Далее этот перевод проверил верификатор.
Axiom Math: «Эта теорема в настоящее время представляет собой предел человеческих знаний о простых числах».
Уже не является. Вот 240 уже, а не 246. https://arxiv.org/abs/2608.31126
ИИ использовали для проверки самого сложного на сегодняшний день математического доказательства