ИИ Aristotle решил математическую задачу Эрдёша!
ИИ-система Aristotle от стартапа Harmonic впервые самостоятельно решила открытую математическую задачу. На решение задачи Эрдёша #124, сформулированной в 1995–1997 годах, потребовалось 6 часов. Еще минута ушла на формальную проверку доказательства в системе Lean. Участие человека ограничилось постановкой задачи.
Harmonic разрабатывает концепцию "математического сверхинтеллекта" (MSI) — ИИ, способного работать с формальным языком Lean4 и автоматически верифицировать свои доказательства, что минимизирует вероятность ошибок. В ноябре стартап привлек $120 млн при оценке $1.45 млрд, а одним из сооснователей является Влад Тенев, генеральный директор Robinhood. Ранее, в июле, Aristotle продемонстрировал уровень золотой медали на Международной математической олимпиаде, успешно решив 5 из 6 задач.
Стоит отметить, что Эрдёш сформулировал две версии задачи #124: упрощенную (с разрешенными единицами) и оригинальную, более сложную (с запретом на использование единиц и дополнительным условием на НОД оснований). Aristotle решила упрощенную версию. Математик Борис Алексеев, который передал задачу ИИ, подчеркнул, что доказательство оказалось неожиданно простым, хотя математики не могли найти его в течение почти 30 лет.
Aristotle является частью более масштабной системы формализации математики. Задачи берутся из каталога Эрдёша, который ведет Томас Блум, формальные постановки — из проекта Google DeepMind Formal Conjectures, языковые модели (например, ChatGPT) преобразуют статьи и доказательства в LaTeX, а Lean осуществляет проверку. Борис Алексеев рассказал, как организовал эту систему: в одном из экспериментов конвейер ChatGPT + Aristotle обработал около десяти задач Эрдёша, начиная с формулировки и заканчивая готовым доказательством, верифицированным Lean.
Итак, ИИ решил задачу, которую люди не могли 30 лет. Похоже, скоро нам всем придется переписывать учебники математики, потому что кто знает, какие еще гениальные решения припрятаны в глубинах машинного кода? Просто иронично, что теперь машина умнее нас в нашей же области.
