Если раньше математика держалась на простом принципе «убедил коллег, значит доказал», теперь принцип получил опасного двойника. ИИ уже научился писать доказательства так уверенно и гладко, что тексты выглядят безупречно даже в местах, где спрятана ошибка. Математики все чаще спрашивают себя, как не принять красивую подачу за истину, особенно когда «красиво» пишет машина.
Повод для тревоги появился после закрытой встречи в 2025 году. На встрече ведущие специалисты по математике тестировали модель OpenAI o4-mini. По словам участников, ответы звучали так, будто текст пишет живой исследователь, который ведет мысль и удерживает в голове сложную конструкцию доказательства. Профессор теории чисел Кен Оно из Университета Вирджинии вспоминал, что раньше не встречал у моделей подобной манеры рассуждать, и сравнил увиденное с работой ученого.
Чем убедительнее звучит машина, тем проще продавить слабое место в логике. Кен Оно прямо признавал, что модель способна выдавать правдоподобные, но неверные решения. По формулировке Кена Оно, o4-mini освоила «доказательство запугиванием» когда авторитетная подача заставляет читателя сомневаться не в тексте, а в собственной компетентности.
Математик Терри Тао из UCLA объясняет проблему проще. Раньше стиль служил сигналом качества. Слабый математик обычно пишет хуже и расставляет акценты мимо цели. С ИИ сигнал ломается. Модель идеально имитирует форму строгого рассуждения и при этом ошибается, оставаясь одинаково убедительной в обоих вариантах. Отсюда страх получить поток «железобетонных» доказательств с тонкими изъянами, которые трудно поймать человеческим глазом.
На первый взгляд тема кажется внутренней болью математиков, но ставки остаются прикладными. Если в основе результата лежит сомнительное доказательство, результатом нельзя подпитывать следующие инструменты, теоремы и методы. Часть задач, включая знаменитую проблему P против NP, упирается в подобные краеугольные доказательства. Успех меняет практику от логистики и проектирования микросхем до криптографии.
При этом идея доказательства всегда оставалась немного «социальной». Доказательство считают принятым, когда другие математики проверили шаги и согласились с корректностью каждого перехода. Механизм работает, но не дает гарантии абсолютной истины. Математик Эндрю Гранвилл из Монреальского университета подозревает, что даже в хорошо изученных работах встречаются проблемы, иногда из-за формулировок и языковых нюансов.
История напоминает, что ошибаются и отдельные люди, и коллективный восторг. В 1993 году Эндрю Уайлс представил доказательство Великой теоремы Ферма после лет почти полной изоляции, и мир уже праздновал победу над задачей, которая простояла 350 лет. Во время рецензирования рецензенты нашли в доказательстве существенную дыру. Эндрю Уайлсу понадобился еще год, чтобы закрыть дыру. Некоторое время «доказанная» теорема фактически оставалась недоказанной.
Один из ответов на новую угрозу математики видят в формальной верификации. Формальная верификация переводит доказательство в строгий формальный язык, затем компьютер проверяет каждый шаг по правилам логики и не пропускает ни одного неясного места. Самый известный инструмент такого типа называется Lean. Подход убирает двусмысленность человеческого текста и заставляет доказательство проходить механическую проверку.
В такой связке ИИ может стать помощником, а не источником риска. Терри Тао считает, что принуждение модели выдавать результат сразу в проверяемом формальном формате снимает большую часть проблемы «убедительно, но неверно». Математик Кевин Баззард из Имперского колледжа Лондона описывает сценарий как диалог. Lean указывает на ошибку, ИИ переписывает шаг, цикл повторяется до прохождения проверки.
У будущего есть философская сторона. Если ИИ научится строить формально корректные доказательства настолько сложные, что ни один человек не сможет осмыслить доказательство целиком, возникнет вопрос о природе полученного знания. Кевин Баззард напоминает, что математика уже сталкивалась с неполным пониманием, когда большую статью пишут десятки авторов, а каждый держит в голове только собственный фрагмент. Были и компьютерно-ассистированные доказательства, например теорема о четырех красках, которая со временем стала нормой и попала в учебники. Но сценарий, где машина предлагает доказательство, чинит доказательство и проверяет доказательство, а человек лишь фиксирует прохождение формальной проверки, выглядит новой территорией. Математикам предстоит решить, где проходит граница между знанием и корректно выполненной процедурой.