Недавно в математическом сообществе прогремели одна за одной новости о том, как LLM решают неподдавшиеся людям математические проблемы. Так в мае GPT-5.6 Sol смогла найти контрпример к гипотезе Эрдёша, потом она же опровергла гипотезу из теории графов в 3 страницы (!!!), а на днях Fable опровергла 87-летнюю гипотезу Якоби.

Да, нахождение контрпримеров это в некотором роде брутфорсинг, который отдавать LLM - самое милое дело, может показаться, что это не есть какой-то прорыв.

Например для доказательства гипотезы из теории графов OpenAI запустили 64 агента и приказали им работать “как минимум 8 часов, прежде чем сдаться”. Полный промпт можно найти тут.

Но в статье профессора из Имперского колледжа Лондона можно увидеть намного большие возможности: для опровержения гипотезы Эрдёша Sol не просто искала контрпример, а конструировала его с помощью нескольких глубоких теорем, а далее смогла даже описать его на языке Lean, который используется для формализации доказательств (про него можно отдельную статью настрочить), в 1.2 миллиона строк за 3 недели работы. В это же время математическая библиотека самого Lean насчитывает 2.3 миллиона строк, которые писали 9 лет.

Что это всё значит? Математиков тоже заменят? Об этом тоже рано говорить. Новостей о том, как LLM доказала бы действительно сложную гипотезу с нуля, следуя всем математическим и логическим нормам, ещё нет, да и без человеческого контроля пока что никуда, но предпосылки появления таких возможностей в будущем уже видны.

Но избавление математиков от казавшегося ранее несбрасываемого бремени формализма уже происходит и происходит большими темпами. LLM для оформления своих работ с помощью Lean использует даже Теренс Тао, один из, если не самый, передовой математик нынешнего времени. Говорит он об этом в интервью в прошлом году и жалуется, что в большинстве случаев всё-таки это работает плохо, но в четверти случаев идеально. Может сейчас в этом плане что-то поменялось в лучшую сторону.

Также тот же самый “брутфорсинг” становится всё более и более привлекательно отдавать нейронке, примеров этому, мне кажется, уже вполне достаточно.

Выглядит так, как будто новая эра математики не за горами, так что остаётся только ждать будущих совершенств и открытий.

What a time to be alive.