ИИ Aristotle доказал задачу Эрдеша, вызвав ажиотаж в математическом сообществе

Стартап Harmonic, основанный CEO Robinhood Владом Теневым, представил впечатляющий результат: их ИИ Aristotle самостоятельно доказал задачу Эрдеша №124, используя формальную систему Lean Prover.

Ранее Aristotle продемонстрировал свои способности, получив золотую медаль на международной математической олимпиаде.

Борис Алексеев, математик-исследователь, провел тестирование бета-версии. Aristotle сгенерировал доказательство за шесть часов, а проверка заняла всего минуту. Кроме того, ИИ исправил опечатку в формулировке задачи из проекта Formal Conjectures, немного усложнив ее решение.

Несмотря на то, что математическое сообщество считает, что Aristotle решил упрощенную версию задачи из BEGL96, успех ИИ вызывает большой интерес. Математик Томас Блум предлагает оставить задачу Эрдеша №124 нерешенной, а решение ИИ вынести в связанные проблемы.

В социальных сетях обсуждается, что работа ИИ сопоставима с уровнем олимпиадных задач, и высказываются предположения о возможной утечке данных из тренировочных материалов. Однако, наибольший интерес представляет автоматизированный процесс генерации доказательств в Lean Prover без непосредственного участия человека – это рассматривается как значительный шаг в области математического моделирования.