Полтора века гипотезу Римана щупали сильнейшие математики планеты — и так ни разу и не дотянулись. Теперь новость о доказательстве её ослабленной версии, квазигипотезы Римана, пришла, как сообщается, не с университетской кафедры, а из команды разработчиков ИИ: рассуждение, по имеющимся данным, выстроила языковая модель. Классическая гипотеза остаётся открытой, но расклад уже другой. Строгие доказательства, похоже, перестали быть монополией человека.
Гипотеза Римана родом из 1859 года. Она утверждает, что нули дзета-функции выстраиваются на одной прямой — критической. На этой прямой держится вся аналитическая теория чисел, а Фонд Клея положил задачу в список «проблем тысячелетия» с миллионом долларов за решение.
До недавнего времени полигоном для ИИ были олимпиадные задачи. В 2024 году AlphaProof вместе с AlphaGeometry взяли результат уровня серебра Международной математической олимпиады. Через год модель Gemini уровня Deep Think решила пять задач из шести — официально засчитанное золото.
Квазигипотеза — следующая ступень. Как сообщается, она касается широкого класса функций, похожих на дзета-функцию, и для них аналог утверждения Римана доказан. Ослабленный результат, разумеется, не тянет на доказательство классической гипотезы. Но если всё подтвердится, дистанция между «олимпиадным упражнением» и работой на переднем крае науки впервые сократится до одного шага. Главный вопрос теперь — проверка: машинное рассуждение математикам предстоит разобрать построчно.
Скептикам и возражать не надо: языковые модели умеют уверенно галлюцинировать, подавая правдоподобное за верное. У математики на это давно готов ответ — формальная верификация. Прецедент старше всяких нейросетей: компьютерное доказательство теоремы о четырёх красках появилось ещё в 1976 году, а десятилетия спустя его целиком перепроверили в системе Coq. Сегодня фактический стандарт — пруф-ассистент Lean. Доказательство записывается как программа, и машина проверяет её корректность относительно аксиом и правил вывода, не пропуская ни единого шага. Педант, каких поискать.
Схема «ИИ предлагает — верификатор подтверждает» снимает главную претензию к нейросетям: черновик модели может быть кривым, но формализованный текст либо проходит проверку, либо нет. Тонкое место — сама формализация. Переведёшь утверждение криво — и докажешь вовсе не то, что имелось в виду. Поэтому без людей пока никуда: поставить задачу, выверить формулировку, осмыслить результат — всё это по-прежнему работа математика.
За пределами математики ИИ уже приносил фундаментальной науке куш: AlphaFold закрыла проблему предсказания структуры белков, а её создатели уехали с Нобелевской премией по химии. В 2025-м AlphaEvolve улучшила алгоритмы умножения матриц — над этой задачей люди бились десятилетиями. Математика идёт той же дорогой: Теренс Тао, один из сильнейших математиков современности, ведёт проекты по массовому формализованию теорем и без обиняков называет нейросети новым исследовательским инструментом.
Показателен и Liquid Tensor Experiment: сообщество формализаторов в Lean полностью проверило сложнейшее доказательство Петера Шольце, которое вручную до того считалось непроверяемым. Меняется сам формат науки. Математик всё чаще — постановщик и редактор, машина — генератор вариантов и строгий проверяющий. Осталась и щекотливая сторона: журналы и жюри уже требуют расшифровывать, что именно сделала модель. Эта этика только складывается.
Кадровая база для «машинной математики» здесь историческая: институт Стеклова, мехматы ведущих университетов, олимпиадная традиция, вырастившая не одно поколение исследователей. Есть и собственные наработки в формальных методах — средства верификации программ в стране развивают десятилетиями.
С большими языковыми моделями картина другая: GigaChat у Сбера и YandexGPT у Яндекса развиваются быстро, но публичных систем автоматического доказательства уровня AlphaProof в стране пока нет — появится ли, вопрос открытый. Перспектива, впрочем, прозрачна: соединить сильную математическую школу с прикладным ИИ. Вот только как быстро это случится, зависит от кучи обстоятельств, и предсказать их никто не возьмётся.
Если сообщение о квазигипотезе подтвердится, в историю эпизод войдёт, скорее всего, не результатом — тот всё равно промежуточный, — а методом: машина доказывает, формальный верификатор ручается, человек ставит вопрос и отвечает за смысл. В такой связке научное соавторство перестаёт быть метафорой. Гипотеза Римана в полном виде, возможно, продержится ещё долго, но потолок для ИИ уже не там, где был вчера. Спорить дальше будут не о том, способна ли модель доказывать теоремы, — о том, как доверять ей задачи посложнее.