ИИ-математик Aristotle доказал одну из нерешенных проблем из списка Эрдеша (но с оговоркой)

Если вы в первый раз слышите про Aristotle, рассказываем: это система от стартапа Harmonic, основанного в 2023 году. Ребята занимаются ИИ в математике, уже получили немало инвестиций, и продукт у них довольно интересный.

Он отличается тем, что генерирует не просто текст доказательства: вместо этого Aristotle пишет формальное доказательство в среде Lean, то есть сочетает в себе formal verification и informal reasoning + search.

Ну так вот. На днях создатели объявили о том, что модель решила проблему Эрдеша номер 124. Эта задача впервые была выдвинута в статье «Полные последовательности множеств целых степеней» в журнале Acta Arithmetica почти 30 лет назад и с тех пор считается открытой.

Aristotle же потратил на задачу 6 часов и решил ее абсолютно без участия человека. Потрясающе? Потрясающе.

Вот только оказалось, что версия задачи, которую решил Aristotle, отличается – это упрощенный вариант. Оригинальная формулировка была несколько другой и допускает увеличение степени только начиная с определенной, не включая единичную. В той формулировке задача остается нерешенной. И хотя результат действительно крутой, прорыва (сюрприз-сюрприз) снова не произошло 😭

Все это в который раз доказывает: да, какую-то новую математику модельки уже способны доказывать. Но это, что называется, «низко висящие плоды» – то есть довольно простые по меркам академии утверждения уровня среднего аспиранта или олимпиадника. До гипотезы Римана им еще как пешком до Китая.

Кстати, после распространения новости в соцсетях завирусился новый термин «vibe-proving» – как vibe-coding, только для математиков 💡