ИИ в математике — системы искусственного интеллекта, которые доказывают теоремы, решают олимпиадные и исследовательские задачи и проверяют доказательства. Ключевую роль играет формальный язык Lean: доказательство на нём проверяет компьютер, поэтому результат ИИ можно проверить без доверия к самой модели.
За три года область прошла путь от олимпиадного уровня серебряной медали (2024) до сотен рукописей с новыми результатами (2026).12 Это вызвало у математиков и восторг, и тревогу: Теренс Тао говорит о наступлении «эпохи изобилия доказательств», а Международный математический союз поддержал декларацию о том, что математика должна оставаться человеческим делом.34
История
- 14.12.2023Google DeepMind публикует в Nature систему FunSearch: языковая модель вместе с автоматической проверкой нашла новые конструкции больших cap set — лучше известных ранее.5 ¶ cza2rk877
- 25.07.2024Системы DeepMind AlphaProof и AlphaGeometry 2 решают четыре из шести задач Международной математической олимпиады — 28 баллов, уровень серебряной медали; одну задачу за минуты, остальные — до трёх дней. AlphaProof соединяет предобученную языковую модель с алгоритмом обучения с подкреплением AlphaZero и доказывает утверждения на Lean.1 ¶ cpmp95wjd
- 14.05.2025DeepMind AlphaEvolve находит способ умножать комплексные матрицы 4×4 за 48 скалярных умножений — лучше алгоритма Штрассена 1969 года. На 50 с лишним открытых задачах система примерно в 75% случаев повторила лучшие известные решения, а в 20% улучшила их.6 ¶ cz2yux3ij
- 19.07.2025OpenAI заявляет, что её экспериментальная модель рассуждений показала на олимпиаде результат уровня золотой медали.7 ¶ ccp7fkcq7
- 21.07.2025Gemini Deep Think от DeepMind официально получает золото олимпиады: пять задач из шести решены полностью, 35 из 42 баллов, в пределах 4,5 часа соревнования; результат официально оценили и подтвердили координаторы олимпиады по тем же критериям, что и решения школьников.8 ¶ c4xkfkcjr
- 08.09.2026OpenAI сообщает, что её внутренняя модель доказала возможность сингулярности в уравнениях Навье — Стокса (со внешней силой), задействовав около 10 000 агентов за 88 часов; доказательство формализовано в Lean.9 ¶ cfknhmsr6
- 08.10.2026В Science выходит статья DeepMind об агенте AlphaProof Nexus: он сам решил 9 из 353 открытых задач Эрдёша и доказал 44 из 492 гипотез энциклопедии целочисленных последовательностей OEIS, все доказательства проверены в Lean. В том же номере математики Джереми Авигад и Мэтью Баллард пишут колонку «ИИ для исследовательской математики уже здесь».10 ¶ ckdzaxmkz
Как устроено
Есть два подхода. В первом модель ищет решения в виде программ или конструкций, а автоматический оценщик проверяет, лучше ли они известных: так работают FunSearch и AlphaEvolve. Во втором модель пишет доказательство на формальном языке Lean, и его проверяет компьютер: так устроены AlphaProof и проект Gauss компании Math Inc, который за три недели формализовал сильную форму теоремы о распределении простых чисел — около 25 000 строк Lean — по задаче, поставленной Тао и Алексом Конторовичем в январе 2024 года.11 ¶ c6575vwd8
Данные
| исследование | что измеряли | результат |
|---|---|---|
| Epoch AI, FrontierMath, 07.11.202412 | новые сложные задачи уровня исследовательской математики | лучшие модели решали меньше 2% задач ¶ cc9ttcnpr |
| OpenAI, 06.10.20262 | результаты внутренней модели, выложенные на GitHub; оценка самой компании | 719 рукописей в 372 группах, около 4000 поставленных задач; один результат в среднем — около трёх часов работы ChatGPT Pro в режиме размышления; три рукописи вскоре отозваны из-за ошибки в знаке ¶ cghjnybxm |
За два года ИИ прошёл путь от «меньше 2%» на исследовательских задачах и олимпиадного серебра до сотен рукописей с новыми результатами. Проверяемость — главное отличие математики от других областей: доказательство на Lean проверяет компьютер, поэтому скорость ИИ здесь упирается не в доверие к модели, а в способность людей понять и встроить результаты. Оговорки: часть заявлений — внутренние оценки компаний, а самые громкие результаты OpenAI выпущены моделью, которую нельзя проверить снаружи. ¶ c8xxc87et
Критика
В октябре 2025 года исследователи сообщили, что с помощью GPT-5 нашли решения 10 задач Эрдёша, числившихся открытыми. Хранитель базы erdosproblems.com Томас Блум назвал подачу «драматическим искажением»: GPT-5 нашёл уже опубликованные статьи с решениями, о которых он лично не знал, а статус «открыта» означал лишь, что ему такая статья неизвестна. По его словам, умение модели искать литературу «и так полезно и впечатляет — незачем выдавать его за то, чем оно не является».13 ¶ cydu4nn57
После выпуска OpenAI The Verge поговорил с более чем тремя десятками математиков; Бартош Наскренцкий сказал, что это «может привести к огромному обвалу академической культуры».14 ¶ c6fm7zxay
Scientific American 13.10.2026 рассказал, что математики, разобрав 166-страничное доказательство OpenAI для уравнений Навье — Стокса, увидели: внешняя сила в нём построена совсем иначе, чем в программе испанских математиков Диего Кордобы и Луиса Мартинеса-Соровы, — хотя при выпуске компания «ясно и неоднократно» заявляла, что следует их программе.15 ¶ cdpxcquac
Тимоти Гауэрс назвал свой главный страх по поводу ИИ в математике «возможным разрушением математической культуры» — знаний и опыта, которые существуют не только в литературе, но и в головах математиков.16 ¶ czth2y863
Развитие
02.06.2026 опубликована Лейденская декларация об ИИ и математике, которую поддержал Международный математический союз: заслуги и ответственность за результаты остаются за людьми и не должны приписываться автоматическим системам.4 ¶ cxrzjmjxp
Тао предлагает перестать слепо гнаться за решением задач: в эпоху изобилия доказательств это, по его словам, уже вредит долгосрочному здоровью математики.3
Сигналы
- Наука / Джек Кларк: «ИИ становится творческим — и в математике, и в исследованиях самого ИИ, поэтому полное рекурсивное самоулучшение теперь скорее станет возможным в 2027 году, а не в 2028-м»сооснователь Anthropic, в своей рассылке Import AI — о тесте исследовательского чутья моделей; в мае он оценивал в 60% вероятность, что к концу 2028 года модель сможет сама обучить себе преемника
- Наука / Теренс Тао: «Мы вступаем в эпоху изобилия доказательств»в лекции «Math 2.0» в Калтехе — о том, что ИИ сделал с математикой
- Наука / Юго Дюминиль-Копен: «Выпуск OpenAI сотен ИИ-доказательств — «монументальный шок»: для математиков «наступил следующий день»; на одной из его задач — будто бежал марафон с кем-то на спине, кто спрыгнул за 100 метров до финиша и пересёк черту первым»французский математик, лауреат Филдсовской премии 2022 года, — в эфире швейцарского радио RTS после того, как OpenAI выложила сотни рукописей с доказательствами ИИ, 16 из них — по задачам его области
- Наука / Тимоти Гауэрс: «Доказать то, чего не могут доказать LLM»филдсовский лауреат — о том, что ChatGPT за час сделал исследование уровня диссертации
См. также
Примечания
-
AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind, 25.07.2024. deepmind.google ↩ ↩2
-
openai/math — OpenAI, GitHub, 06.10.2026. github.com ↩ ↩2
-
Math 2.0 — Terence Tao, 10.10.2026. terrytao.wordpress.com ↩ ↩2
-
Leiden Declaration on Artificial Intelligence and Mathematics — 02.06.2026. leidendeclaration.ai ↩ ↩2
-
B. Romera-Paredes et al. Mathematical discoveries from program search with large language models — Nature, 14.12.2023. nature.com ↩
-
AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms — Google DeepMind, 14.05.2025. deepmind.google ↩
-
Alexander Wei: «our latest @OpenAI experimental reasoning LLM has achieved … gold medal-level performance» — X, 19.07.2025. x.com ↩
-
Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad — Google DeepMind, 21.07.2025. deepmind.google ↩
-
On the Navier–Stokes Millennium Prize Problem — OpenAI, 08.09.2026. openai.com ↩
-
Tsoukalas et al. Advancing mathematics research with AI-driven formal proof search — Science, 08.10.2026. doi.org ↩
-
Introducing Gauss, an agent for autoformalization — Math, Inc. math.inc ↩
-
E. Glazer et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI — arXiv, 07.11.2024. arxiv.org ↩
-
Thomas Bloom: «this is a dramatic misrepresentation» — X, 17.10.2025. x.com ↩
-
‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop — The Verge, 09.10.2026. theverge.com ↩
-
OpenAI’s blockbuster Navier-Stokes proof isn’t what we thought it was — Scientific American, 13.10.2026. scientificamerican.com ↩
-
Thoughts about the Leiden Declaration — Timothy Gowers, 26.07.2026. gowers.wordpress.com ↩