Рог математического изобилия

Чистая математика — работа человеческого разума, которая в то же время подчиняется строгим правилами логики. Естественно ожидать, что как раз в этой области искусственный интеллект мог бы себя проявить. Но только в последние месяцы чат-боты навострились решать открытые задачи, то есть такие, ответов на которые раньше не существовало нигде. Насколько хороши эти решения — и что будет дальше?

Очень много вопросов

Математик Пал Эрдёш написал множество статей, в которых не только доказал сотни теорем, но и поставил . На некоторые из них математики нашли ответы, а другие так и остались открытыми.

Задачи Эрдёша — как решенные, так и нет — собраны на одноименном сайте, который создал Томас Блум из Манчестерского университета. Предложить дополнение или исправление к его содержанию может каждый. К проекту неоднократно привлекал внимание в своем блоге Теренс Тао — известный математик, которому интересны и коллаборативные математические проекты, и наследие Эрдёша. Небезразличен Тао и к применению современных технологий машинного обучения к чистой математике.

При поддержке Тао сайт приобрел известность в математической среде, и с этим удачно совпали еще несколько обстоятельств:

• Это каталог вопросов, поставленных известным математиком прошлого, так что их можно считать хотя бы немного известными и интересными;
• Среди них много нерешенных;
• за полнотой и актуальностью коллекции задач бережно следят, как и за точностью формулировок;
• Практически все задачи понятны без узкоспециальных знаний;
• Условия и — часто — решения задач хорошо поддаются формализации, то есть переписыванию в формате, понятном компьютерной программе, которая может подтвердить правильность доказательства.

Под влиянием этих факторов задачи Эрдёша превратились в бенчмарк математических способностей ИИ: энтузиасты применяли общедоступные чат-боты к нерешенным вопросам из списка и делились результатами там же в комментариях.

Первых успехов они добились в конце 2025 года, когда с помощью ChatGPT некоторые открытые проблемы удалось перевести в категорию решенных. Правда, успехом это можно было назвать только с оговорками: в некоторых случаях ИИ проделал исключительно хорошую работу по поиску уже существующего решения; в иных же случаях он как будто находил собственное решение, но при ближайшем рассмотрении оказывалось, что оно все-таки уже где-то встречалось — а разработчики приложили большие усилия, чтобы языковые модели все научные статьи и книги, которые когда-либо были оцифрованы.

Чтобы ориентироваться в потоке новых результатов, в конце прошлого года Теренс Тао создал на GitHub страницу, где начал собирать информацию о вкладе ИИ в решение задач Эрдёша. Поначалу в разделе, озаглавленном «Самостоятельный вклад ИИ. Наличие литературы: сопоставимая литература неизвестна. Человеческое участие: незначительно» не было ни одной строчки, отмеченной зеленым — то есть указывающей, что чат-бот предложил полное решение задачи. Но продолжалось это недолго.

Первопроходцы

К концу 2025 года Кевин Баррету, 21-летний второкурсник-математик из Кембриджского университета, уже несколько месяцев регулярно тестировал способности новейших языковых моделей к математическим рассуждениям. Когда вышла ChatGPT-5.2 Thinking, он понял, что по сравнению с предшественниками и конкурентами она способна на большее. К тому времени у Баррету уже был опыт с задачами Эрдёша: он справился с открытой задачей под номером 481 и даже формализовал решение — правда, выяснилось, что решение этой задачи уже было в литературе.

Теперь же Баррету и его приятель Лиам Прайс, 23-летний любитель математики, вооружились ChatGPT-5.2 Pro — еще более продвинутым вариантом модели, доступ к которому получили от знакомых, и стали испытывать его на разных открытых задачах Эрдёша. И уже в начале января 2026 года (после еще одной осечки, подобной истории с задачей номер 481), их усилия принесли результат: первую полностью автономно решенную ИИ задачу Эрдёша под номером 728.

Решение задачи номер 728 от Баррету, Прайса и ChatGPT получилось сравнительно кратким и, главное, было формализовано, поэтому никто не сомневался, что оно верно. Все сошлись во мнении, что задача не была особенно уж сложной и оставалась нерешенной лишь потому, что никто из математиков не взялся поработать над ней действительно серьезно. Но все же первый математический результат, практически полностью автономно полученный ИИ, стал знаковым.

Баррету рассказал, как выстроил работу с языковыми моделями:

• Первым делом он использовал ChatGPT Deep Research или Gemini Deep Research для поиска по литературе — чтобы убедиться, что задача действительно еще не решена, и собрать все полезные сведения о ней.
• Затем Баррету начинал диалог с «решателем» (solver) — ChatGPT Pro. Он сообщал ему точное условие задачи и всю релевантную информацию, собранную на начальном этапе, и при этом .
• После этого «решатель» выдавал полное и, скорее всего, неверное решение. Баррету не проверял его самостоятельно, а поручал это дело трем «ИИ-контролерам» (checker) с доступом в интернет: двум копиям ChatGPT Pro и одной Gemini Deep Think. Полученные замечания он передавал чат-боту без доступа к интернету, чтобы тот внес исправления. Цикл повторялся до тех пор, пока хотя бы один «контролер» не соглашался, что решение верное.
• В случае успеха Баррету позволял «решателю» пользоваться интернетом, и цикл продолжался до тех пор, пока все три «контролера» не признавали верность результата.
• Далее следует тонкий момент. Бывает, что найденное решение задачи на самом деле эксплуатирует лазейки в формулировке и не отвечает на суть вопроса. Поэтому требуется отдельный, новый «контролер», который получает на вход задачу, решение и запрос: действительно ли решена именно та задача, которую, скорее всего, имел в виду автор? Если ответ «нет», то все приходится начинать сначала. 
• Если же решение прошло все проверки, то дальше его можно формализовать с помощью специализированной модели.

Чтобы пропустить через этот конвейер сотни задач, Баррету предлагает также использовать ИИ-агента — Codex (родственник ChatGPT) или Claude Code.

Успеху Кевина Баррету способствовало несколько факторов:

• Он обладал математической подготовкой и знал, что делает;
• Он использовал хорошую ИИ-модель — скажем, с бесплатной версией ChatGPT получить такой результат было бы совершенно невозможно;
• Он придумал хороший алгоритм работы;
• Он нашел способ устранить всякие сомнения в истинности результата — формализовал решение;
• Наконец, он удачно выбрал такую задачу, к решению которой, несмотря на ее простоту, будет интерес — просто потому, что это одна из Задач Эрдёша.

Быстрее, лучше, сложнее

На первопроходцев немедленно обрушилось внимание со стороны математиков, журналистов и разработчиков ИИ. Это помогло и им, и другим энтузиастам применения искусственного интеллекта в математике развить успех.

В январе 2026 года Баррету с несколькими соавторами решили задачу Эрдёша . Для этого они использовали  — ИИ-агента от Google DeepMind, в основе которого лежит языковая модель Gemini, а алгоритм его работы, по-видимому, был вдохновлен доказавшим эффективность подходом Баррету. С помощью Aletheia компания Google и сотрудничающие с ней математики получили еще ряд результатов разного уровня. Доступа к агенту у обычных пользователей нет ни бесплатно, ни по подписке.

Были и другие успехи. Так, недавно Лиам Прайс доказал с помощью ChatGPT-5.4 Pro теорему о , которая позволила, помимо прочего, решить еще две задачи Эрдёша.

А самого громкого на данный момент результата добились в компании OpenAI с помощью пока закрытой для общего использования модели — опровержение гипотезы Эрдёша о . Гипотеза звучит так: пусть имеется n точек на плоскости; посчитаем количество пар точек, находящихся на расстоянии ровно 1 друг от друга; тогда это количество — не более чем порядка n.

На первый взгляд кажется, что это должно быть верно: чтобы получить как можно больше пар на расстоянии 1, хочется расположить их в какую-нибудь регулярную решетку, например квадратную или треугольную, и тогда количество пар на расстоянии 1 будет приблизительно 2n или 3n соответственно — то есть действительно порядка n. Однако ИИ показал, что можно добиться количества пар порядка n^a, где a есть некоторое число строго больше 1 — стало быть, больше, чем порядка n.

Этот результат примечателен как минимум по двум причинам. Во-первых, гипотеза о единичных расстояниях — это действительно известная и сложная задача. Предложенное моделью от OpenAI решение далеко не тривиально и, несомненно, может быть опубликовано в математических журналах. Во-вторых, статья OpenAI уже показывает одно из наилучших возможных свойств научных работ: она не только предлагает решение задачи, но и становится основой для новых статей, уже целиком подготовленных людьми (включая Томаса Блума), в которых методы из доказательства от OpenAI применяются к новым задачам.

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

«Поверить алгеброй гармонию»

Поговорим наконец и о формализации, которая пока оставалась в тени. Любой человек, попытавшийся применить языковые модели к чему-то вроде математических задач, немедленно сталкивается с проблемой: ИИ относительно быстро может сгенерировать много текста, который необходимо проверять на истинность. Вот только у экспертов-людей совершенно нет мотивации этим заниматься, особенно если пользователь, получивший у ИИ решение, — никому не известный студент, как Кевин Баррету.

Вообще-то это абсурдная ситуация: вся суть компьютеров в том, что они умеют рассуждать безошибочно — и вдруг именно компьютерная математика оказывается ненадежной и требующей проверки. К счастью, здесь могут помочь уже не языковые модели, а обычные компьютерные программы. Например, Lean — интерактивная система-помощник для формализации и проверки теорем с открытым исходным кодом. Она отличается от аналогов в первую очередь мощной централизованной библиотекой определений и доказанных теорем Mathlib, большой популярностью, а также отсутствием багов математического «ядра».

Конечно, чтобы программа могла проверить доказательство, нужно сначала переписать его с человеческого языка на машинный. Этот процесс называется формализацией. Формализация доказательства всегда была довольно трудоемким и непопулярным занятием.

Большие языковые модели стали производить много математического текста — потенциально ценного, но наполненного ошибками. Вот тут-то формализация и проверка стали актуальными как никогда. Для некоторых языковых моделей, предназначенных , язык системы Lean даже был «родным»: на нем модели тренировалась и общались. Однако со временем самые впечатляющие математические результаты стали выдавать неспециализированные ИИ-модели, «просто» прочитавшие весь интернет, книги и научные статьи.

Таким образом, чтобы избежать необходимости тратить время и труд людей-экспертов на проверку математических результатов, полученных большими языковыми моделями, нужно формализовать их и переложить работу по верификации на систему проверки доказательств. Но этот маневр будет иметь смысл только в том случае, если формализацией также займется ИИ. С этим пока не все гладко: из-за того, что Lean очень быстро развивается и меняется, недостаточно хорошо справляются с этой задачей.

Поэтому для автоформализации лучше использовать специализированные ИИ-инструменты. На этом поле два основных игрока, и оба выдают код для Lean. Первый — общедоступный и бесплатный Aristotle от компании Harmonic. Именно его Кевин Баррету применял к решению задачи номер 728, и похоже, что этому примеру полезно по возможности всегда следовать при работе с доказательствами, выданными искусственным интеллектом.

Второй известный инструмент автоформализации — Gauss от компании . Эта система гораздо мощнее Aristotle: при поддержке команды математиков она может быстро формализовать довольно большие и сложные доказательства на сотни тысяч строк кода. Однако воспользоваться ей могут немногие: Gauss — внутренний продукт компании.

У Math Inc. весьма амбициозные планы по автоформализации известных математических доказательств, вплоть до классификации простых конечных групп. Впрочем, публикация полного организованного доказательства классификации пока так и не завершена, и ходят слухи, что в ее доказательстве был обнаружен пробел. Так или иначе, последний громкий успех Math Inc. — формализация доказательства Марины Вязовской о плотнейших упаковках шаров в 8- и 24-мерном пространствах.

Если доказательство автоформализовано, это еще не гарантия, что оно верно: при формализации доказываемых утверждений может быть допущена ошибка (а раз утверждение — не то, что было нужно, то уже неважно, доказано оно или нет). Кроме того, ИИ может эксплуатировать некоторые известные трюки, чтобы утверждение лишь выглядело доказанным. Например, в Lean есть директива «считать это утверждение верным без доказательства» под смешным названием «sorry» — и понятно, что через эту директиву можно «доказать» вообще что угодно. Тем не менее убедиться в отсутствии таких проблем гораздо быстрее и проще, чем проверить доказательство, записанное обычным человеческим языком. Именно поэтому первые решения задач Эрдёша, полученные от ChatGPT, были приняты безо всяких сомнений: они были формализованы.

Осознание и реакция

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

Многие из них скептически или неприязненно относятся к компаниям-разработчикам, в частности, подозревая, что они . К тому же на каждое успешно выполненное ИИ нетривиальное доказательство приходятся тысячи безуспешных или тривиальных. Пользователи-нематематики зачастую неспособны отличить одно от другого и выдают бессмысленный нейрослоп за математические прорывы, что тоже может создавать для профессионалов видимость бесполезности языковых моделей. Есть и ученые, которые не отрицают возможностей ИИ, но сознательно не хотят иметь с ним дела просто потому, что находят вдохновение в самостоятельном научном поиске.

Опубликованную 2 июня Лейденскую декларацию об искусственном интеллекте и математике подписали более двух тысячи ученых. Преамбула документа пронизана беспокойством и тревогой. В ней авторы перечисляют «потенциальные угрозы», которые ИИ представляет для математики:

• выдача правдоподобных, но ошибочных рассуждений;
• использование чужих результатов без должного цитирования;
• потрясения для систем академического найма и финансирования — ученые, не желающие использовать ИИ, окажутся в проигрышном положении;
• публикация математических результатов посредством блогов и пресс-релизов (как это иногда делают технологические компании), а не статей в рецензируемых научных журналах, препятствует их «должной оценке»;
• получение технологическими компаниями контроля над математическими исследованиями.

Подписи под документом оставили в том числе люди, которые относятся к языковым моделям с энтузиазмом, например Теренс Тао и Кевин Баррету. Однако, к примеру, Дэниел Литт не соглашается с отдельными идеями документа: обязательным атрибутированием результатов людям, даже если их полностью получил ИИ, или акцентом на публикацию в форме традиционных научных статей.

Экстраполяция

Математики, наиболее пристально следящие за успехами ИИ, такие как Теренс Тао, Дэниел Литт или сэр Тимоти Гауэрс, практически не сомневаются, что уже в обозримом будущем доказательство теорем — одна из основных составляющих работы математиков-исследователей — сможет быть полностью делегирована компьютерам: если цель — доказать теорему, то практически всегда быстрее и проще будет доверить это ИИ. 

При этом все перечисленные люди — не мечтатели. Ими движет вполне благородный интерес к новым возможностям, а также прагматизм: они не хотят упустить возможность делать больше математики, хорошей и разной, реалистично оценивая текущие возможности новых инструментов. В некоторых разделах математики уже возможна продуктивная совместная работа человека и машины: обмен идеями, помощь от ИИ в технических моментах доказательства лемм и ускорение тем самым работы человека.

В то же время пока реальные успехи ИИ сконцентрированы в задачах типа эрдёшевских. Математика велика и разнообразна, а полезность передового ИИ крайне неоднородна. К примеру, из первого этапа проекта First Proof относилась к области бесконечномерной теории меры, и она осталась нерешенной. Чрезвычайно упрощая, можно сказать, что задачи и решения, в которых ИИ наиболее хорош, часто сводятся к последовательному рассмотрению конечного набора случаев — к комбинаторике; а в математической среде есть давняя традиция смотреть на комбинаторику свысока.

В любом случае резонно ожидать, что темпы производства основного формального продукта математической научной работы — научных статей, отправленных в рецензируемые научные журналы — станет выше. Это означает, что вырастет нагрузка на журналы и традиционная модель публикаций перестанет справляться с обработкой поступающих математических работ (не то чтобы она блестяще справлялась уже сейчас).

Возможное решение этой проблемы — значительно более широкое внедрение формализации. Можно представить себе мир, в котором престижные математические журналы требуют, чтобы статья была дополнена формализованным доказательством. Тогда с плеч рецензентов, будь они людьми или языковыми моделями, можно будет снять огромную часть работы по рецензированию — проверку верности рассуждений и результатов.

Впрочем, формализацию и автоформализацию сообщество математиков тоже не воспринимает как безусловное добро. Даже до эпохи больших языковых моделей на формализацию часто смотрели свысока — еще в большей степени, чем на комбинаторику. Автоформализация теоремы о плотнейшей упаковке шаров и вовсе буквально огорошила редакторов Mathlib: они сочли ее . Тем не менее, разработчики Lean и Mathlib быстро сориентировались и запустили инициативу «Формальный фронтир», призванную сделать автоформализацию полезной для всех — так сказать, не бороться, а возглавить.

Споры о том, как искусственный интеллект встроится в мир математики и перестроит его, продолжаются. Тем временем языковые модели показывают все более впечатляющие результаты — и не похоже, что этот процесс будет замедляться.