- ИИ-система Aristotle, разработанная стартапом Harmonic, впервые полностью автономно решила открытую математическую задачу из каталога Пола Эрдёша.
- Решена слабая версия задачи Эрдёша №124, которая оставалась нерешённой почти 30 лет, решение заняло 6 часов и было формально верифицировано в системе Lean за минуту.
- Aristotle — часть комплексного конвейера формализации математики, в котором задействованы языковые модели и формальные системы для автоматизации доказательств.
Современные достижения в области искусственного интеллекта демонстрируют значительный прогресс в формальной математике. Стартап Harmonic представил систему Aristotle — интеллектуальный агент, обладающий способностями «математического сверхинтеллекта», — который впервые полностью автономно решил открытую математическую задачу из каталога Пола Эрдёша. Конкретно речь идёт о задаче №124, сформулированной в период 1995–1997 годов.
Важно подчеркнуть, что Aristotle справился с так называемой слабой версией задачи, допускающей использование единиц измерения, в отличие от оригинальной формулировки, запрещающей их и вводящей дополнительное условие на наибольший общий делитель оснований. Несмотря на то, что решена была не самая жёсткая модификация, подмножество задачи оставалось открытым более трёх десятилетий, а предоставленное решение оказалось достаточно простым, чего не смогли достичь профессиональные математики.
Процесс решения занял у системы около шести часов автономных вычислений, после чего подтверждение корректности было формально верифицировано в Lean — специализированной формальной системе — за одну минуту. Отметим, что человек участвовал лишь в постановке задачи и проверке результата, что подчёркивает уровень независимости ИИ в данном процессе.
Aristotle функционирует на базе языка Lean4 и встроен в широкий конвейер формализации математических доказательств. В его работу интегрированы проекты Google DeepMind Formal Conjectures для формальной постановки задач, а также языковые модели, подобные ChatGPT, которые переводят математические статьи и доказательства в формат LaTeX для последующей проверки Lean. Данный конвейер позволяет автоматически обрабатывать задачи, расширяя базу формально проверенных доказательств и стимулируя дальнейшее развитие автоматизированной математики.
Кроме того, за последние периоды Aristotle уже формализовал более десяти известных математических утверждений, не создавая новые решения, а переводя классические доказательства в машинно-проверяемый код. Это обеспечивает надёжность и reproducibility научных результатов, а также служит фундаментом для все более сложных автономных математических исследований.
Финансово проект Harmonic поддержан крупными инвесторами: в ноябре стартап привлёк $120 миллионов при оценке в $1,45 миллиарда. Среди сооснователей компании — известные фигуры в индустрии, такие как Влад Тенев, CEO Robinhood. В июле нынешнего года Aristotle достиг уровня золотой медали на Международной математической олимпиаде, решив 5 из 6 олимпиадных задач, что является подтверждением высоких интеллектуальных возможностей системы.
Таким образом, прорыв системы Aristotle в решении задач, остававшихся без ответа десятилетиями, демонстрирует не только технические возможности искусственного интеллекта, но и открывает перспективы для ускоренного развития математики с помощью формальных машинных методов. Это знаменует новый этап в синергии математики и ИИ, когда машины не только поддерживают исследователей, но и самостоятельно вносят вклад в науку.
