1 декабря, то есть буквально в этом месяце, с помощью ИИ была решена ещё одна проблема Эрдёша

Она оставалась нерешённой на протяжении 30 лет. А решила её система Aristotle. Чуть подробнее о ней:

Это ИИ-система от стартапа Harmonic. Она не работает сама по себе и фигурирует лишь на одном из этапов многоступенчатого пайплайна.

Одним из ключевых инструментов также является Lean — это язык программирования и система для формальной верификации математических доказательств, в которой доказательства записываются как программы и автоматически проверяются на логическую корректность. Это позволяет получать строгие, машинно-проверяемые доказательства теорем.

Ещё важную роль играет проект DeepMind Formal Conjectures, который занимается систематическим переводом математических задач из естественного языка в формальные объекты, пригодные для работы в системах вроде Lean. По сути, это корпус формализованных гипотез и заготовок для будущих доказательств, с единым представлением задач, с которым могут напрямую работать ИИ-агенты.

Вот как примерно выглядят весь «конвейер» формализации, доказательства и последующей верификации результата:

берутся задачи из каталога Эрдёша

DeepMind Formal Conjectures связывает их с Lean-совместимыми формальными утверждениями и заготовками для дальнейшей формализации

языковые модели (вроде ChatGPT) помогают автоматизировать доработку дальнейшей формализации, генерируя дополняющие куски Lean-кода с целью привести задачу к итоговому машиночитаемому варианту

Aristotle работает в связке со всеми предыдущими инструментами, генерируя формальные доказательства на основе полученных формализаций; корректность каждого шага механически проверяется в среде Lean

Так вот, Aristotle полностью решил одну из версий задачи Эрдёша №124, поставленной в середине 1990-х. Сделал он это примерно за 6 часов, а формальную проверку доказательства Lean выполнил всего за минуту.

Отметим, что была решена «слабая» версия, поэтому в базе задача всё ещё числится нерешённой. Хоть эффективное доказательство и оказалось неожиданно простым, нельзя отрицать, что обнаружил его именно ИИ.

Здесь подмигиваем оптимистам, оставившим 🦄 под вчерашней публикацией.

Не проходит и суток, как один из создателей Aristotle сообщает о решении проблемы №481. Новость «взрывает» реддит. В комменты приходит автор доказательства и делится деталями работы.

Оказалось, что на самом деле работа по активному привлечению Aristotle началась ещё в ноябре. Например, тогда вышло опровержение второй части проблемы №367, которое, как вы можете догадаться, проверил именно ИИ

Кстати, произошло это всё с подачи математика Бориса Алексеева. Подробный рассказ из первых уст был опубликован 5 декабря.

А уже 8 декабря в блоге Теренса Тао выходит обстоятельный лонгрид о решении ещё одной проблемы — №1026. В нём можно проследить, как решение становится синтезом человеческой работы и ИИ.

Согласитесь, звучит впечатляюще! Но волнения в математическом сообществе присутствуют, что вполне понятно. Трудно представить, насколько иной станет математика в эпоху vibe proving.

И что же всё это значит

Можно предположить, что роль математика в будущем сместится в сторону архитектора доказательств. Человек выбирает определения, задаёт направления исследования и нажимает «пуск». Уже сейчас в соцсетях можно наблюдать, как любители экспериментируют с этой ролью и получают любопытные результаты.

Однако у этого романтизированного взгляда есть обратная сторона. В системах формализации иногда получаются доказательства, которые могут быть практически неинтерпретируемы для человека.

Хорошо ли, когда столь мощные системы получают результаты, которые мы не в состоянии понять? Решать вам!

#история