
Новости с заголовком «ИИ решил задачу тысячелетия» стали появляться всё чаще. Со стороны бывает сложно оценить: где исторический прецедент, а где надуманный хайп? А главное: что всё это значит для будущего математики?
Чтобы внести в вопрос ясность, полезно послушать самих математиков. Что они считают подходящими для ИИ задачами, а что — человеческими? В чём видят прогресс, а в чём — обыкновенный инфоповод? В чём вообще их видение смысла математики и как теперь, в изменившемся мире, подходить к математике сознательно?
Мы в Kodik занимаемся не математикой, а редактором кода с ИИ. Тем не менее, в нашей команде есть люди с классическим мехмат-образованием, и мы с интересом следим за темой. Поэтому ранее переводили мнения математиков про опровержение конкретной задачи Эрдёша, а теперь решили осветить их взгляд на происходящее в целом. Конечно, мнения расходятся, но в этой статье мы попробовали собрать срез математического сообщества.
Предмет обсуждения важный, поэтому статья объёмная. Ёмкая версия для тех, кто торопится:
У передовых LLM стремительно растут способности к математическим доказательствам. В 2025-м ИИ не находил новых доказательств, в начале 2026-го стал получать малозначимые, а теперь в случае с уравнениями Навье — Стокса заявлено о решении одной из семи «задач тысячелетия», и утверждается, что почти взята ещё одна. До ИИ человечество сумело одолеть только одну из таких задач (гипотезу Пуанкаре).
Это не значит, что ИИ уже может доказать вообще всё, но меняет конъюнктуру. Люди стали забрасывать ИИ-моделям все открытые задачи подряд. Многие попытки были безуспешными, однако из успешных результатов возник целый поток. Теренс Тао назвал это наступлением «эпохи изобилия доказательств»: в математике доказательства всегда были в дефиците — и потому ценными — теперь ценность смещается в другие аспекты работы.
Доказательства — лишь часть того, чем занимаются математики, в других аспектах ИИ пока что слабее. Сейчас LLM не создают новых теорий, а публикации о доказательствах пишут хуже людей. Их решения — обычно использование уже известных подходов, а не концептуальные прорывы. Поэтому математики не считают, что ИИ «обошёл во всём». Но именно доказательства ранее были «мерилом успеха» для людей, что заставляет пересматривать ситуацию.
Поскольку рост способностей ИИ продолжается, сейчас мы наблюдаем не финальную форму развития. Уже понятно, что математика видоизменится, но по вопросу «какой именно окажется в итоге» в математическом сообществе идут жаркие дискуссии.
Пока что понятно, что формальная валидация становится важнее. Когда машины генерируют много результатов (среди которых немало и галлюцинаций), а люди публикуют их в интернете без полноценного peer review, новым боттлнеком вместо доказательств оказывается их проверка. Поэтому становятся всё важнее те инструменты, которые помогают с проверкой фактической ценности очередных открытий. Среди таких инструментов верификации популярностью пользуется Lean.
Мнения математиков по поводу ИИ различаются: есть как сторонники его использования, так и противники. Главным коллективным заявлением стала «Лейденская декларация», которая обозначает возможные проблемы при использовании ИИ, но не призывает бойкотировать его, а даёт рекомендации по его использованию. Например, декларация рекомендует математику-исследователю раскрывать факт использования ИИ в работе; нести ответственность за результат и помогать другим проверять его.
Многие критикуют конкретные применения ИИ, а не ИИ в математике вообще. Возникла ситуация, напоминающая «золотую лихорадку», из-за чего всё чаще наспех публикуют недопроверенные решения и некачественные тексты, расходящиеся с ценностями академического мира. В адрес OpenAI звучат обвинения в том, что они могли частично «списать» результат с Навье — Стоксом у живых математиков, консультировавшихся с их моделью. Пока трудно сказать, продлится ли подобный период долго или эффект «лихорадки» вскоре пройдёт, а более вдумчивое использование ИИ останется.
Среди математиков возникло много дискуссий, связанных не только с самим ИИ. Например, если машины забирают на себя ту задачу, по которой ранее оценивался академический успех, возникает метавопрос: по каким критериям оценивать научную ценность? Как правильно организовывать научный процесс?
Часть математиков убеждена, что оценка учёного по количеству доказательств всегда была некорректным подходом, потому как первоначальная цель в понимании, а не в количестве созданных PDF-файлов. Новым обсуждаемым вопросом стал следующий: «Каковы вообще цели фундаментальной математики?» С прикладной всё ясно, так как её результаты осязаемы, а зачем именно заниматься «классической математикой» без каких-либо практических применений — дискуссионная тема.
Этот вопрос был важен и до ИИ, но теперь многое зависит от ответа на него. Например, если вдруг ИИ найдёт доказательство гипотезы Римана и верифицирует миллионами строк на Lean, но никто из людей не сможет его осознать, что такое событие будет значить для математики?
Однозначных ответов пока нет, но существуют предложения «в какую сторону двигаться». К примеру, Теренс Тао заявил, что математике пришло время переосмыслить себя, выделил ряд этапов в жизненном цикле доказательств и подчеркнул, что люди всегда приоритезировали первый («получить доказательство»). Теперь приходит время сосредоточиться на других: от «проверить» до, как он выражается, «каноникализировать».
А теперь рассмотрим всё это в подробностях:
Чтобы ощутить темпы прогресса, полезно посмотреть, как всё развивалось со временем. Вот лишь часть заметных событий:
2022 год: появляется ChatGPT, и люди начинают активно обсуждать возможности LLM. Но даже на простейшие задачи вида «у Васи было 5 яблок» модель может уверенно давать неправильные ответы. Так что обычно считается, что в математике этому «стохастическому попугаю» делать нечего.
2024 год: представлена первая reasoning-модель OpenAI o1-preview, а позже DeepSeek R1 популяризирует этот подход. При создании таких моделей используется обучение с подкреплением, значительно улучшая результаты в математических бенчмарках.
2025 год: После проведения Международной математической олимпиады сразу и OpenAI, и DeepMind заявляют, что их модели справились с задачами на уровне золотой медали. Но олимпиадные результаты — ещё не научные прорывы, а к методологии возникают вопросы. Так что прогресс уже заметен, но математики очень осторожны в его оценках.
Октябрь 2025 года: сотрудник OpenAI заявляет, что их модель нашла доказательства для некоторых задач Эрдёша. Но затем оказывается, что эти доказательства уже были известны человечеству, и модель обнаружила существовавшие, а не дошла до собственных. Многие скептически высказываются в духе «ИИ только плагиатить и может».
Начало 2026 года: а вот теперь на erdosproblems.com действительно появляются первые доказательства открытых задач, полученные с помощью ИИ. Поначалу речь идёт о малоизвестных задачах, на которые люди ранее попросту не тратили много времени. То есть результат реальный, но малозначимый.
Февраль 2026 года: заявляет о себе проект First Proof, призванный проверять способности моделей на новых математических задачах. Он создан в академическом мире и не зависит от коммерческих компаний вроде OpenAI, что повышает его авторитет среди математиков. В феврале у него в качестве теста был опубликован первый набор задач, и ИИ справились с частью из них. Позже последовали два новых набора.
28 февраля 2026-го: Дональд Кнут со словами «Шок! Шок!» сообщает, что Opus 4.6 помог ему в работе над новым томом «The Art of Programming», найдя решение интересовавшей его задачи. Кнут пишет, что теперь ему придётся «пересмотреть свои взгляды на генеративный ИИ».
20 мая 2026-го: компания OpenAI сообщает, что её новая модель опровергла гипотезу Эрдёша о единичном расстоянии. Этой гипотезой ранее безуспешно занимались многие люди. Поэтому математики сходятся на том, что вот это уже по-настоящему значимый результат (вплоть до формулировки «если вы математик, сейчас присядьте»).
2 июня 2026-го: публикуется коллективная Лейденская декларация. В ней математики пишут, что ИИ может очень повлиять на будущее области, и среди специалистов это вызывает разные эмоции от энтузиазма до тревоги. Они предлагают ряд мер для математиков, организаций и государств, с которыми использование ИИ должно быть благотворнее для области.
20 июля 2026-го: сотрудник Anthropic твитит, что пока он смотрел финал футбольного чемпионата, модель Fable по его запросу опровергла известную проблему якобиана. Найденный контрпример он прикладывает прямо в твите. Теперь значимые доказательства есть не только на счету моделей OpenAI.
1 августа 2026-го: компания OpenAI представляет сразу 10 доказательств, найденных моделью Astra, на тот момент недоступной публично. Математики пишут, что если бы эти доказательства были найдены людьми, то многие из них заслуживали бы публикаций в ведущих журналах. А если бы все они ещё и были от одного человека, это означало бы для него звёздную карьеру.
4 сентября 2026-го: Anthropic заявляют о проделанной формализации доказательства Великой теоремы Ферма в Lean. Само доказательство давно было известно, но это самый масштабный проект автоформализации: ИИ-модель написала миллионы строк на Lean.
8 сентября 2026-го: OpenAI заявляют, что с новой моделью получили результат для уравнений Навье — Стокса, достаточный для статуса «решённой задачи тысячелетия» от института Клэя. Если результат будет официально подтверждён, это первое за 20 лет решение «Millennium Prize Problem».
10 сентября 2026-го: OpenAI заявляют, что близки к решению ещё одной «задачи тысячелетия» и скоро поделятся результатом.
Прогресс очевиден. Но у многих возникает такой вопрос: а в чём именно ИИ становятся всё лучше? Если они справляются с целым рядом задач, но не всеми, то чем эта часть отличается от других? Как это соотносится с человеческими способностями?
Например, обладатель премии Филдса Тимоти Гауэрс в августе написал пост «What sort of maths are LLMs good at?». Попробуем дальше просуммировать тезисы из многих подобных постов.
Многим людям хочется получить простой ответ: «Так что, LLM стали способнее математиков?» Но на самом деле вопрос не сводится к бинарному «да/нет»: в математике занимаются очень разными вещами, а у ИИ есть как преимущества, так и недостатки. Если посмотреть «что упоминают в числе того и другого», можно встретить такие варианты:
Широта познаний. Математика очень разнообразная, и ни один человек не знает её «целиком». Обычно математики работают «в глубину», специализируясь на конкретной области и пытаясь продвинуться в ней как можно дальше. Но это может мешать, когда в рамках одного доказательства нужно соединить подходы из разных областей. Возможно, у человечества уже есть нужные знания, но они ещё не «сходились в одной голове». А вот модель, обученная на всех данных сразу, может заметить неочевидную связь. Она работает «в ширину».
Меньшая предубеждённость. Когда ИИ опроверг гипотезу Эрдёша о единичных расстояниях, некоторые математики предположили, что человечество ранее находилось под излишним влиянием авторитетов. Сам Эрдёш считал, что гипотеза верна, поэтому обычно её пытались именно доказать, а на попытки опровержения тратили мало ресурсов — вот ничего и не получалось. А для машины Эрдёш не такой авторитет, она готова тратить время на его опровержение, и это помогло. Напрашивается вопрос: а в каких ещё задачах мы не достигли результата только из-за того, что излишне доверяем сложившимся мнениям? Сколько мифов помогут разрушить LLM?
Скорость работы. Быстрая машина может «пытаться применить все известные подходы подряд», в то время как у человека это заняло бы слишком много времени. Это что же получается, побеждают просто скучный брутфорс и мощное железо? Не совсем: ведь пару лет назад GPU уже были быстрыми, а LLM и близко не показывали нынешних результатов. Качество применяемых подходов возросло, и без этого ничего не получилось бы. Но и количество важно. Как в 90-х произошло с шахматами, когда для победы над человеком помогли улучшения и в алгоритмах, и в железе.
Неутомимость. Похоже на предыдущий пункт, но стоит упомянуть и отдельно. Если человек совершает много попыток и не получает результата, он может оказаться демотивирован и переключиться на другое, «а то вся жизнь так пройдёт». А машине можно всегда говорить «пробуй ещё». Забавный факт: в некоторых случаях достичь нового доказательства получалось после того, как после первых неудач в следующих промптах писали буквально «верь в себя, не сдавайся».
Способности к росту в верицифируемых областях. Обучение с подкреплением хорошо работает, когда машине можно давать чёткий сигнал «справляешься ты или нет». Для задачи «сочини стихотворный шедевр» это плохо подходит (люди расходятся во мнениях, что является шедевром). А вот математика гораздо более подходящая, позволяет подавать примеры целыми пачками, в том числе формально верифицированные. Также она удобна тем, что может происходить «целиком внутри компьютера». С другими науками сложнее: как только требуется ставить эксперименты «в реальном мире», LLM уже не может настолько ускорять процесс быстрыми вычислениями.
Уклон в контрпримеры. Когда гипотеза Эрдёша была опровергнута, ИИ помогло не только то, что люди слепо доверяли авторитету. Сыграло на руку и то, что опровержение — менее впечатляющий результат. Контрпримеры сейчас находят один за другим, а вот с доказательствами истинности пока что всё не настолько активно. Поэтому, пока одни восторгаются новостями, другие задаются вопросом: среди ошибочных гипотез теперь многое опровергнут, а вот с истинными-то что будет, их сумеем доказать или нет?
Меньше глубины. Как уже написали, ИИ лезет «не столько вглубь, сколько вширь». Поэтому его доказательства впечатляют многих математиков («Я над этой задачей когда-то сам бился и не осилил»), но обычно не как «гениальные озарения». Чаще можно увидеть реакцию вроде «Здорово, но вообще мы могли бы и сами догадаться, подходы-то известные использованы». А ведь доказательства в математике ценны не только сами по себе: в процессе их поиска могут возникать новые теории и подходы, развивающие науку в целом. И вот таких прорывов от ИИ пока не видно. Возникнут ли они позже? С текущими темпа роста многие этого ожидают, но никто не знает точно.
Качество публикаций. Недостаточно найти доказательство само по себе: чтобы оно пошло на пользу математике в целом, нужно ещё корректно описать его для других. И в описаниях ИИ сейчас слабее, например, уделяет недостаточно внимания сложным переходам. Также нередко «забывает» поставить ссылки на чужие работы, словно доказывал всё с нуля, а не опирался на предшествовавшие результаты. Это нарушает научный этикет, так что людям требуется перепроверять подобное за машинами.
Ошибки и неудачи. Заголовки об успехах впечатляют, но для корректной картины мира надо помнить, что в них не попадает множество неудачных попыток, когда LLM жгут токены безрезультатно или вовсе галлюцинируют. Из задач Эрдёша взят уже целый ряд, но на данный момент гораздо больше остаётся открытыми. Это не умаляет достижений, а просто напоминает, что впереди ещё большой путь.
Цена. Достижения моделей впечатляют, но порой на промптинг тратят гигантские суммы. В случае с уравнениями Навье — Стокса стоимость получения доказательства оценивают в миллионы долларов, и это успешный случай, а сколько ещё в OpenAI потратили безрезультатно? Поэтому математики порой иронизируют: «Да если бы в доказательства раньше столько денег вкладывали, мы бы давно всё сами решили». Впрочем, ИИ-индустрия с годами всё сильно оптимизирует: если в 2019-м обучение модели GPT-2 обошлось в десятки тысяч долларов, сейчас стоимость обучения подобной модели оценивается в $48. Так что и цена математических доказательств может оказаться временной проблемой.
Из-за этих преимуществ и недостатков образовался своеобразный «LLM-подход» к доказательствам, отличающийся от привычного «человеческого».
Отличие «ширина против глубины» сказывается на том, как логично давать задачи машине. Живой математик может поставить важной целью одну задачу, постепенно забираться всё дальше, потратить годы, но в удачном случае добиться-таки результата. А ИИ-модель может взять даже несколько задач за сутки, но если уж не осилила какую-то по своим способностям, то и за год вряд ли с ней справится.
Поэтому к LLM зачастую подходят «наоборот»: не оставляют модель на год с одной задачей, а идут по целому списку. Что-то получится доказать, что-то нет: первому радуются, второе оставляют до следующего поколения моделей, чтобы с ними попробовать снова. В этом году среди людей, применяющих ИИ к задачам Эрдёша, при выходе каждой новой версии GPT возникала целая волна: «О, теперь получилось взять ещё несколько».
Можно встретить такую метафору: работы лучших математиков — словно горные вершины, между которыми остаются долины. А ИИ-доказательства — словно поднимающаяся вода, заполняющая долины. Рекорд высоты она пока что не побила, вершины остаются. Зато захватывает всё, что ниже определённого уровня, а у людей на многое из этого могло не хватать ресурсов.
Кроме того, поскольку у LLM сейчас лучше получается с контрпримерами, в части случаев люди сразу задумываются «какие известные гипотезы с высокой вероятностью окажутся ошибочными», отправляя модели искать их.
А ещё с LLM-доказательствами связан рост популярности проекта Lean, и это стоит рассмотреть отдельно:

Идеи формальной верификации и «автоматических доказательств» появились давно — например, проекту Isabelle уже 40 лет. Но раньше они были нишевыми, а в изменившеся мире стали актуальнее. Особенно часто стало можно услышать про Lean. Этот проект состоит из нескольких компонентов: одноимённого языка программирования, инструмента доказательства теорем на этом языке, а также коллективной библиотеки Mathlib (математики не доказывают каждый шаг «с нуля», а опираются на уже известные результаты, и Mathlib позволяет импортировать их).
Если гипотеза была формализована в Lean, то её доказательство в Lean можно проверить автоматически. Язык был отчасти вдохновлён Haskell, про который ходят полушутки «если проект компилируется, значит, работает». Но тут уже не шутки: цель действительно в том, чтобы важные для людей свойства оказывались надёжно проверены автоматикой.
Проект появился в 2013-м, и тогда его создатель Леонардо де Мура хотел, чтобы отсутствие определённых багов в софте можно было не просто проверять отдельными тестами, а гарантированно доказывать. Ни про какой ИИ он тогда и не думал.
Всё довольно быстро пошло не по плану: основными пользователями стали не программисты, а те математики, которым была близка идея проверяемых доказательств. Но поначалу их сообщество было маленьким. Доказательство на языке Lean занимает во много раз больше строк, чем обычной математической нотацией, и мало кто хотел связываться с непривычным инструментом, когда «и в голове проверить можно».
Теперь же ситуация изменилась. В виде LLM появился мощный инструмент, способный без человека находить непростые доказательства, но также способный галлюцинировать. Когда новые доказательства возникают уже целым потоком, всё сложнее проверять каждое вручную, тратя время на неудачные попытки. И тогда гораздо актуальнее звучит вопрос: а что, если проверки будут автоматическими? Что, если надолго оставлять машину саму доказывать, чтобы человека отвлекали результатом, только когда возникает подтверждённый успех?
И сейчас, когда представляют новое громкое доказательство, зачастую это сопровождается Lean-версией. Когда OpenAI публиковали свои результаты в случае с Навье — Стоксом, на видное место они поместили ссылку на соответствующий репозиторий.
Lean — тоже не панацея от всех бед. Во-первых, в нём самом ранее находили баги, позволяющие «доказать» ошибочные утверждения. Добросовестный математик вряд ли столкнётся с такими багами случайно, они становятся актуальны лишь при желании «перехитрить систему». Но ИИ-моделям как раз свойственно поведение «reward hacking», не могут ли они использовать такое? Поэтому, когда было опубликовано доказательство для Навье — Стокса, специалист по формальной верификации Талия Рингер задалась вопросом: когда ранее формализовали доказательство Великой теоремы Ферма, мы уже знали «оно верное», а тут как исключить тут вероятность бага? Есть проект Lean4Lean для «проверки проверяющего», но пока что ситуация не является разрешённой.
Во-вторых, с Lean можно автоматически проверять доказательство гипотезы, но сначала кому-то требуется формализовать саму гипотезу. При этом возможно допустить ошибку и формализовать ерунду, не соответствующую исходной идее, а тогда в доказательстве будет проверено лишь соответствие этой ерунде. Получается, человеку по-прежнему надо возиться? Частично: ускорить процесс помогает автоформализация, но она не даёт полных гарантий.
В-третьих, даже когда ошибок нет, формализовать можно по-разному. Недавно Anthropic с помощью ИИ формализовали важное старое доказательство Великой теоремы Ферма, и это заняло всего 11 дней, хотя математику Кевину Баззарду на ручное выполнение такой задачи ранее выдали пятилетний грант в миллион фунтов стерлингов. Звучит триумфально, и сам Баззард признал, что его опередили. Но есть нюанс: у ИИ-модели получился Lean-код на целых 13 миллионов строк. Да, это доказательство автоматически проверяется, но у многих возникли вопросы: а нельзя ли сделать гораздо короче, чтобы для живых людей код был доступнее и показательнее? Не окажется ли «дорогая» версия Баззарда куда полезнее?
Однако уже сейчас ситуация выглядит лучше с Lean, чем была бы без. Когда OpenAI представили 10 доказательств сразу, в одном из них люди нашли спорный момент, поставивший под сомнение весь вывод. Но благодаря Lean-версии математики смогли быстро убедиться, что полученный результат всё же остаётся в силе. В текущей гонке, когда доказательства часто представляют без традиционного peer review (иначе другие опередят), такое особенно ценно.

В августе всё оказалось похоже на казино: люди принялись лихорадочно отправлять в ИИ все открытые задачи в надежде первыми получить доказательства. Но со временем эффект новизны пройдёт, а найти интересную неопробованную задачу станет сложно, так что вряд ли это навсегда.
Некоторые математики сейчас возвращаются к задачам, над которыми когда-то безуспешно бились: «Ух ты, теперь ИИ нашёл результат, и он отличается от того, которого я тогда ожидал». Другие говорят, что несмотря на все успехи ИИ, конкретно в их сфере он всё ещё мало что может доказать. Порой они видят пользу, но другую: например, «с ИИ стал удобнее поиск по существующей литературе», «модель нашла в моей публикации ошибку», «я получил частичный результат».
В текущей волне пытаются участвовать не только математики. Например, создатель JS-рантайма Bun Джарред Самнер попросил ИИ-модель доказать гипотезу Римана, и с этим она не справилась, но неожиданно добилась некоторых результатов в связанной с этим гипотезе.
Джарред понимал, что такое выходит за рамки его компетенций, и прежде чем хвастаться результатом, показал его более разбирающимся людям. Но не все подходят так ответственно, и возникло понятие «математический слоп». Кто-то постит ошибочные «доказательства» без понимания, лишь засоряя интернет неверными данными. Кто-то публикует кликбейтные заявления в духе «ИИ уже решил всю математику». А на сайт erdosproblems.com, где собирают решения задач Эрдёша, стало поступать много низкокачественных сообщений, усложняя жизнь создателю сайта Томасу Блуму.
В итоге Блум написал тред о том, как «использовать ИИ с умом». Он ссылается на двух давних контрибьюторов и перечисляет, что они делают правильно: внимательно читают доказательство сами до отправки на сайт, вычищают текст, указывают «что именно было сделано ИИ и что человеком», обходятся без дешёвой сенсационности. По его мнению, в этом случае ИИ помогает математике, а без такого может и вредить. Другой математик Дэвид Пфау пишет, что стоит сделать нормой прикладывать к любому новому доказательству полные диалоги с LLM, которые к нему привели.
Также много претензий возникло к подходам крупных ИИ-компаний. Математик из Anthropic Левент Альпёгге, получая новые доказательства, то публиковал пост из одних лишь знаков «плюс» и «минус» вообще без пояснений, то размещал сгенерированный LLM сопроводительный текст более чем на 100 страниц. Часть математиков ругается: «Это дешёвые выкрутасы, не предоставить с доказательством проработанный текст — неуважение к области».

Ещё больше шумихи наделали обстоятельства, при которых OpenAI опубликовали своё решение «проблемы тысячелетия». Математик Тристан Бакмастер заявил, что с тем же Левентом Альпёгге работал над той же задачей почти год с помощью разных LLM, а когда на горизонте уже показался успех, об этом узнали в OpenAI — и решили срочно опередить.
При этом OpenAI доступны гигантские ресурсы, и для решения задачи там запускали 10 000 ИИ-агентов одновременно, так что отчасти «задавили железом». К тому же при тренировке своей новой модели они гипотетически могли использовать среди прочего и промпты самого Тристана для старой. Неизвестно, произошло ли подобное в реальности, но многих пугает сама возможность: получается, они могли натренироваться на его работе, чтобы в итоге опередить его же и получить всю славу?
В математическом сообществе такое вызвало много гнева. Специально опередить кого-то, кто год бьётся над важной для него задачей — такое привычно для суперконкурентного мира Кремниевой долины, но не принято в академии. А Теренс Тао написал, что доказательство задачи даже не всегда является «хорошим событием»: по-настоящему интересные задачи встречаются редко, работа над ними помогает математикам многое понять, и что будет, если ИИ возьмёт все такие? Зазвучало много заявлений в духе «корпорациям плевать на математику, они просто используют её для маркетинга, даже если в процессе ей вредят».
Однако часть вещей, вызывающих возмущение, может оказаться временной. Математик Алекс Конторович прогнозирует, что со временем ИИ-компании перестанут сами публиковать новые доказательства, потому что это перестанет быть значимым для маркетинга. Его логика: ранее компании хвастались, что их модели стали делать успехи в олимпиадных задачах, но когда этого стало привычным и перестало удивлять людей, шумиха в этом направлении стихла. Того же он ожидает и здесь.
При этом сами LLM, конечно, останутся доступными и способными, так что математики будут пользоваться их возможностями. Но это они могут делать уже по своему разумению, не нарушая тех академических принципов, которые считают важными.
Тут начинается самая сложная и интересная часть. Про текущий момент и ближайшие перспективы поняли, а что ждёт математику в целом? И как разумно заниматься ей в мире с мощным ИИ?
Вопрос сложный по двум причинам. Одна в том, что мы не знаем будущие способности ИИ-моделей. Успех в доказательствах заметен, а сможет ли ИИ на замену решённым задачам найти такие новые, которые были бы очень интересны для математиков? Или достичь концептуального прорыва? Или вовсе «создать новую математику»?
Грант Сандерсон (создатель ютуб-канала 3Blue1Brown) в интервью отметил, что с такими вещами всё сложнее, потому что задача либо доказана, либо нет, а качество «озарений» куда субъективнее. Но дал свой критерий: «если такое произойдёт, мы это заметим не по числам на бенчмарках, а по тому, что у математиков сменится тон разговоров».
А вторая причина затрагивает куда более фундаментальные основы. Что вообще представляет собой математика? Зачем она нужна? Почему люди выделяют на неё ресурсы? Какие составляющие математики важнее людям и больше заслуживают этих ресурсов?
В интернете сейчас встречаются полярные мнения. Люди со стороны порой радуются: «О, наступает золотой век, машины докажут вообще всё!» Но некоторые математики задаются вопросом: «А что, если из-за успеха ИИ академия не обучит следующее поколение математиков, так что в итоге человечество перестанет понимать даже старые доказательства? Такое стало бы не золотым веком, а катастрофой, и нам нужно её избежать».
Чтобы рассуждать о таких вещах, надо идти с самого начала: а почему вообще нам важны эти доказательства? Существуют прикладные вещи, которые очень прямо сказываются на жизни людей, но у большинства открытых гипотез ситуация не такая. Ну предположим, докажет кто-то важную гипотезу, а что именно это нам даст?
Многие видят значимость сложных гипотез в следующем. Для их решения бывает недостаточно существующих подходов. Поэтому, пока над ними бьются, происходят концептуальные прорывы, возникают новые теории, а в итоге человечество узнаёт больше про мир в целом. И найденные пути может потом использовать для решения других задач. То есть гипотеза Римана важна не просто сама по себе, а как потенциальный ключ ко многому другому.
Но такое определение выглядит немного рекурсивным. Нам нужно решать сложные задачи, чтобы потом… мы могли решать больше задач? Всё ещё можно спросить «а зачем это всё».
Отчасти тут присутствует общая сложность фундаментальной науки. Зачастую, занимаясь исследованием из любопытства, учёный сам не знает, какие практические применения у него могут найтись. При этом многие вещи, которые сейчас улучшают нашу жизнь, появились благодаря трудам таких «любопытных людей» из прошлого. Когда Эварист Галуа работал в XIX веке, он понятия не имел, что в XX веке его наработки пригодятся для современной криптографии.
Но помимо этого, многие математики считают, что главная цель фундаментальной математики — понимание само по себе. Доказав известную гипотезу, человечество может потом никак не применить её «практически», но если оно стало чуть больше понимать про мир, то это уже ценно.
Этой весной нашумел пост математика Дэвида Бессиса «The Fall of Theorem Economy». Он заявляет, что математика давно пошла по неправильному пути, когда стала ориентироваться на доказательства как мерило успеха. Люди вроде Годфри Гарольда Харди убедили всех, что находить новое знание превыше всего, а, например, разъяснять чужие результаты и учить им — «задача для второсортных умов».
По мнению Бессиса, куда правильнее высказывался Уильям Тёрстон, который возражал на такое: цель математики — понимание, и оно коллективное, поэтому важна вся деятельность в этом направлении, включая обучение других. Теоремы сами по себе ничего не стоят, мы ценим их только потому, что они важны для людей.
Этот спор возник задолго до современного ИИ, но теперь ИИ делает его по-новому актуальным. Если, как Харди, ставить во главу угла новые доказательства любой ценой, тогда сейчас можно просто радоваться им. Но всё сложнее, если говорить о сообществе и его коллективном понимании, как это делали и Тёрстон, и Бессис, и другие известные математики вроде Питера Шольце.
С ИИ коллективное понимание может обогатиться новыми знаниями, но может и оказаться разрушено, если не осознавать ценность понимания и гнаться только за числом доказательств. Тут недостаточно способной технологии, нужен ещё и разумный человеческий подход. А как именно он должен выглядеть?
Пока одни голоса математиков звучат тревожно, другие стремятся конструктивно решить задачу взаимодействия с ИИ так, чтобы сохранить важное для людей в математике и в итоге улучшить её.
Самый заметный голос — Теренс Тао: обладатель премии Филдса, который занялся вопросом «ИИ в математике» задолго до текущей шумихи. И ещё до новостей про Навье — Стокса он выступил с большой программной речью «Mathematics in the Age of AI» (текстовый формат, видео). Перескажем тут главное.

По мнению Тао, математика сейчас столкнулась с масштабным «переосмыслением себя», подобным тому, которое было столетие назад. Тогда ей пришлось поставить под вопрос многие привычные вещи и признать, что прошлый хаотичный подход был некорректен. Но в итоге она вышла из кризиса более сильной, чем была до него. И сейчас, говорит Тао, может произойти то же самое.
Дальше он предлагает вместо того, чтобы упираться в доказательства, переосмыслить ценность всего и размотать цепочку: вот есть доказательство, а что в связи с ним нам важно? И цепочка у него получается такой:
Первая стадия: найти доказательство. Раньше мы жили в мире, где доказательства были в дефиците, поэтому ценили их. Но теперь мы входим в эпоху «proof abundance», когда доказательства будут литься таким потоком, что только успевай осмыслять. И поэтому каждое из них становится менее ценным, так что акцент сдвигается на следующие стадии.
Вторая стадия: верифицировать доказательство. Процедура peer review и раньше с трудом выдерживала нагрузку, а теперь становится особенно узким местом. Но здесь ИИ тоже будет всё сильнее помогать благодаря формальной верификации. Сложный вопрос в том, будут ли люди понимать громадные формальные конструкции от ИИ. Уже возникли первые доказательства задач Эрдёша, в которых люди пока что не разобрались.
Третья стадия: описать доказательство. Хорошая публикация была важна и до ИИ, чтобы другие математики по-настоящему поняли сложное доказательство и путь автора к нему. А у ИИ с этим пока что слабо: например, LLM может подробно описать тривиальные места из доказательства, но слишком бегло пройтись по ключевым и сложнейшим, к которым у людей и возникают вопросы. Вероятно, качество ИИ-текстов ещё вырастет, но насколько по сравнению с человеческими — неясно.
Четвёртая стадия: принять доказательство. Одни результаты потрясают математиков и позже сказываются на многом, а другие оказываются полузабыты. Это различие зависит от двух сторон: и от автора (какое доказательство и как он описал?), и от сообщества, которое «принимает» или «не принимает» результат. Это коллективная и неторопливая работа. О ней меньше говорят, но для развития математики она тоже важна. И по мнению Тао, тут можно привлекать ИИ как «фильтр» (отсеивать явно малозначимое), но им не заменить полностью интуицию живых математиков. Только людям решать, что важно для людей.
Пятая стадия: «каноникализировать» доказательства. Самые главные доказательства после принятия сообществом попадают в учебники. При этом они проходят процесс осмысления и встраивания их в уже существующий контекст. Это тоже важная работа, о которой мало говорят. (Он намеренно называет её «каноникализация», а не «канонизация», чтобы избежать религиозных коннотаций).
По мнению Тао, самая важная стадия из всех — не первая, а наоборот, последняя. Она определяет тот «математический канон», который известен человечеству. На этом каноне дальше основывают практические применения результатов в разных областях. Например, на этом каноне и обучаются нынешние LLM. Своими текущими успехами они обязаны ему.
И при том, что эту часть Тао видит самой важной, её он считает наименее подходящей для ИИ.
Так что здесь у Тао получается жизнеутверждающий взгляд. Сколько бы гипотез ИИ завтра ни доказал, это решит только первую стадию из пяти, и у живых математиков останется много работы по остальным. А в таком случае и человеческое понимание останется актуальным. Главное — чтобы человечество осознавало этот список задач, а не решило «машины уже всё сделали, людям делать нечего».
Но, конечно, полностью покажет всё только время, и если тема интересна, в будущем явно стоит следить за развитием событий. Мы в Kodik это тоже будем делать.
А пока что, если вам захотелось погрузиться в тему глубже, можете посмотреть, например, список заметных статей про ИИ и математику на сайте Томаса Блума, коллективный блог математиков Proofs and Prompts или лекцию Сергея Николенко.