ИИ в математике: как меняется роль исследователя

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

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

Почему вопрос стал острым именно сейчас

За последний год тема вышла из стадии «интересных демо». По состоянию на 25 июня 2026 года есть уже несколько проверяемых примеров, где ИИ-системы подошли к задачам, которые раньше считались зоной чисто человеческого математического мышления.

Эти примеры нельзя складывать в лозунг «ИИ заменил математиков». У каждого результата свои ограничения: OpenAI говорит о внутренней модели, DeepMind отдельно уточняет, что IMO проверяла присланные решения, а не весь процесс и не саму систему, а препринты требуют независимого воспроизведения. Вместе они показывают сдвиг: ИИ начинает работать уже на уровне исследовательского процесса, а не только как вычислительный ускоритель.

Три роли ИИ в математике

Полезнее говорить о трёх сценариях работы.

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

Второй сценарий — партнёр. Система предлагает гипотезы, ищет контрпримеры, ведёт несколько линий рассуждения, возвращается к неудачным попыткам и помогает собрать черновик доказательства. В этом направлении смотрит AI co-mathematician: авторы описывают асинхронное состояние, память о неудачных гипотезах, поиск литературы и математические артефакты, с которыми может работать человек.

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

Терри Тао предлагает более продуктивный образ: «big mathematics», крупная распределённая работа людей и машин. Сложную задачу можно разрезать на тысячи подзадач; ИИ закрывает рутинные куски, а люди удерживают постановку, стратегию и смысл. Это близко к тому, как мы уже разбирали RMA и AI-агентов для исследовательской математики, только здесь акцент смещается с результата бенчмарка на устройство самой профессии.

Формальная верификация становится слоем доверия

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

Поэтому в центре обсуждения всё чаще оказываются proof assistants: Lean, Isabelle, Rocq и похожие системы. Lean описывает себя как язык программирования и помощник для доказательств, где минимальное доверенное ядро гарантирует корректность формального доказательства. Идея простая: не верить красивому тексту, а заставить доказательство пройти машинную проверку шаг за шагом.

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

Это важная граница для всей темы. Формальная проверка снижает риск поддельной строгости, но не снимает с человека ответственность за постановку. Поэтому соседний материал Toolarium про Lean4Agent и формальную проверку workflow AI-агентов хорошо ложится в тот же кластер: доверие появляется не из сильной модели само по себе, а из проверяемого процесса.

Что остаётся за исследователем

Если ИИ ускоряет поиск, доказательство и формализацию, роль математика не исчезает. Она смещается вверх по цепочке.

Во-первых, человек выбирает задачу. Умение понять, какой вопрос стоит времени, гранта и коллективного внимания, пока не сводится к поиску доказуемого утверждения. В математике много истинных фактов, которые почти никого не волнуют. Хороший исследователь отличает технически закрываемую задачу от задачи, которая меняет понимание области.

Во-вторых, человек оценивает смысл результата. OpenAI в статье про задачу Эрдеша подчёркивает, что важен не только контрпример, но и новая связь между областями математики. Именно люди затем объясняют, чему этот результат нас научил и какие новые вопросы открылись.

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

В-четвёртых, человек должен управлять доступом и нормами. Google запустила AI for Math Initiative с пятью крупными партнёрскими институтами и доступом к технологиям DeepMind. Это полезно для сильных групп, но поднимает неприятный вопрос: не станет ли передовая математика зависеть от закрытых моделей, дорогого вычислительного бюджета и корпоративных программ доступа.

Риски для образования и мотивации

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

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

Для исследователей риск другой. Если финансирование и престиж начнут измеряться скоростью генерации результатов, медленная работа над пониманием может стать плохо защищаемой. IEEE Spectrum приводит именно этот страх: если компьютер делает большие куски работы, хватит ли у человека мотивации годами разбираться в трудной идее?

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

Где проходит разумная граница

Практическая граница выглядит так: ИИ полезен там, где результат можно независимо проверить и понять. Он опасен там, где человек принимает красивый вывод за знание.

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

Такой же сдвиг виден за пределами математики. В статье про OpenAI LifeSciBench и научных ИИ-агентов мы уже писали, что научный агент ценен не тогда, когда красиво рассуждает, а когда его вклад можно проверить в рабочем процессе. Математика просто показывает эту проблему в наиболее жёсткой форме: либо доказательство держится, либо нет.

Короткий FAQ

Заменит ли ИИ математиков?

Сейчас корректнее говорить о перераспределении работы. ИИ уже берёт на себя часть поиска, вычислений, формализации и чернового доказательства. Но выбор задач, проверка смысла, постановка утверждений и объяснение результата остаются человеческими узлами процесса.

Зачем нужна формальная верификация доказательств?

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

Чем AI-партнёр отличается от AI-оракула?

Партнёр помогает двигаться по задаче так, что человек видит ход рассуждения, может проверять промежуточные шаги и учится на результате. Оракул выдаёт ответ, который приходится принимать на веру или проверять уже постфактум. Для математики первый сценарий усиливает исследователя, второй легко превращает его в оператора чужой системы.

Вывод

ИИ в математике уже меняет роль исследователя, но не отменяет её. Самая ценная работа смещается от одиночного героического поиска каждого шага к организации проверяемого процесса: выбрать задачу, разбить её на части, привлечь модели и proof assistants, понять результат и объяснить его людям.

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

Источники

• IEEE Spectrum: What it Means to Be a Mathematician When AI Does the Math, 25 июня 2026.
• OpenAI: An OpenAI model has disproved a central conjecture in discrete geometry, 20 мая 2026.
• Google DeepMind: Gemini Deep Think at IMO 2025, 21 июля 2025.
• Google: AI for Math Initiative, 29 октября 2025.
• AI co-mathematician: Accelerating mathematicians with agentic AI, arXiv:2605.06651.
• Math Inc: Completing the formal proof of higher-dimensional sphere packing.
• Lean Programming Language.
• Terence Tao: Mathematical methods and human thought in the age of AI, 29 марта 2026.