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