Математик Джорди Уильямсон считает, что ИИ даст доказательства без понимания

ИИ будет всё чаще давать доказательства, за которыми не стоит человеческое понимание, и математикам придётся пересмотреть, что они ценят, — пишет Джорди Уильямсон в записках к своей лекции на Международном конгрессе математиков¹.

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

Повод: Уильямсон, математик из Сиднейского университета, прочитал публичную лекцию «ИИ и долгий разговор человечества» 26 июля в Филадельфии. Записки к ней на 16 страниц он выложил на arXiv 9 октября и дополнил тем, что случилось после лекции.

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

Расклад: Уильямсон перечисляет, чего за несколько месяцев добились ИИ-системы в математике:

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

Общая картина: происходящее Уильямсон объясняет законом Гудхарта: когда показатель становится целью, он перестаёт быть хорошим показателем. Цель математика, по его мнению, — понимание, а доказательство служило его проверяемой заменой. Связь между ними слабеет уже полвека:

• В 1976 году теорему о четырёх красках свели к перебору тысяч случаев, который проверил компьютер, и спор шёл не о верности доказательства, а о понимании.
• В 2016 году компьютер доказал гипотезу о булевых пифагоровых тройках, и это доказательство занимает 200 терабайт.

Сообщество такие случаи нехотя приняло, но урок не усвоило, считает Уильямсон: «Всё более мощные системы будут давать доказательства без понимания». Математикам, по его словам, придётся перестроить стимулы под то, что они на самом деле ценят, и объяснить это обществу и политикам. «Это будет болезненный процесс», — пишет он.

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

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

Но: лучшую картину возможностей моделей в исследовательской математике, по мнению Уильямсона, даёт бенчмарк First Proof, а он существует слишком недолго, чтобы строить по нему прогнозы. В нём математики присылают неопубликованные утверждения из текущих работ, модели получают одну попытку, а решения проверяют рецензенты-люди.

Что дальше: в First Proof уже идёт третий раунд, а итоги второго показали возможности моделей на июнь 2026 года. Когда подведут итоги третьего, Уильямсон не пишет.

При этом Уильямсон уверен, что человеческая математика «выживет и будет процветать». Записки, по его словам, написаны без ИИ: ChatGPT помогал только подобрать ссылки и вычитать текст.