ИИ меняет математику. Почему формальная проверка доказательств не гарантирует их достоверность

Искусственный интеллект ускоряет математические исследования, помогая создавать и проверять доказательства, которые могут занимать сотни страниц и быть практически нечитаемыми для человека. Чтобы подтвердить корректность результатов, ИИ-компании используют Lean — систему формальной верификации, способную проверять математические рассуждения с высокой логической строгостью. Однако новые исследования выявили проблему: даже если Lean успешно проверяет доказательство, это ещё не означает, что машинный код точно отражает исходное математическое утверждение. Более того, ошибки в самой системе проверки способны привести к принятию недействительных доказательств.

«Система гораздо менее совершенна, чем можно было бы ожидать, если мы придаём ей столько значения», — отмечает Сильвен Ридо-Кикучи, логик из Высшей нормальной школы в Париже.

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

Компьютерная формализация предложила альтернативный способ проверки. Математическое доказательство переводится на специальный язык, в котором каждый логический переход должен соответствовать формальным правилам. Программа проверяет полученную конструкцию и устанавливает, следует ли заключение из принятых предпосылок в рамках заданной формальной системы.

Однако здесь есть принципиальная оговорка: проверка машинного доказательства и проверка того, что оно соответствует исходному тексту, — две разные задачи.

От математического текста к машинному доказательству

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

«Когда вы записываете доказательство на естественном языке, например английском или французском, в рассуждениях могут оставаться пробелы. При формализации приходится гораздо точнее объяснять каждый шаг», — говорит Уэсли Фуснер, исследователь Института компьютерных наук Чешской академии наук.

До недавнего времени этот процесс требовал огромных трудозатрат. Например, формализация доказательства гипотезы Кеплера о наиболее плотной упаковке сфер потребовала почти двух десятилетий работы и примерно 500 тыс. строк кода.

Но развитие ИИ существенно ускорило перевод математических текстов в формальный код. В одном из недавних проектов модель Claude компании Anthropic за 11 дней выполнила автоформализацию доказательства последней теоремы Ферма, опубликованного Эндрю Уайлсом в 1995 году. Объём полученного формального представления составил около 13 млн строк.

Одним из основных инструментов такой работы стал Lean — система формализации математики и проверки доказательств, первоначально разработанная в Microsoft Research в 2013 году. Она позволяет описывать математические объекты, утверждения и доказательства на специальном языке, а затем проверять их с помощью формального ядра.

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

«Возможно, статья не имеет смысла, но у нас есть формализация, значит, всё правильно», — так Ридо-Кикучи описывает опасный способ рассуждения, который может возникнуть при чрезмерном доверии к результатам автоматической проверки.

Когда Lean доказывает не то, что утверждает математик

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

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

Именно такую проблему исследовали Андерс Хансен и Фабиан Сирчелли из Кембриджского университета и Александр Бастоунис из Королевского колледжа Лондона. В сентябре 2026 года, после объявления OpenAI о доказательстве, связанном с проблемой Навье — Стокса, они изучили формальное доказательство, подготовленное с использованием Lean.

За три недели исследователи рассмотрели 180-страничное формальное доказательство, применяя ChatGPT для поиска возможных расхождений между текстом на естественном языке и его машинной формализацией. Подробно изучив лишь две страницы, они обнаружили два однозначных примера, в которых формализованное утверждение было слабее соответствующей формулировки в исходном тексте.

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

В препринте «Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs» авторы рассматривают и более фундаментальную проблему. Они утверждают, что достоверная автоформализация неоднозначных математических текстов может быть вычислительно чрезвычайно сложной задачей. Их анализ показывает, что для некоторых классов утверждений сложность разрешения неоднозначностей выходит далеко за пределы обычных алгоритмических задач.

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

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

Может ли ошибаться сама система проверки?

Есть и вторая проблема: даже правильно формализованное доказательство нуждается в надёжном проверяющем программном обеспечении.

Lean использует небольшое доверенное ядро, которое проверяет соответствие доказательства формальным правилам. Такая архитектура призвана минимизировать объём кода, которому необходимо доверять. Однако программные ошибки в ядре могут нарушить это свойство и привести к принятию недействительных доказательств.

В частности, в Lean 4 обнаруживали ошибки, позволявшие специально сформированным программным конструкциям обходить некоторые проверки. В отдельных случаях исследователям удавалось построить формальное доказательство противоречия, которое система ошибочно принимала.

Такие уязвимости называют нарушениями корректности, или soundness bugs. Они опасны тем, что программа может принять доказательство утверждения, которое в действительности не следует из правил используемой логической системы.

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

Создатель Lean, специалист по компьютерным наукам Леонардо де Моура, работающий в Amazon Web Services, признаёт, что полностью исключить появление новых ошибок трудно. Поэтому безопасность системы требует не только исправления известных дефектов, но и постоянного тестирования, независимых проверок и совершенствования архитектуры.

Важно, однако, не смешивать обнаруженные уязвимости с утверждением, что все версии Lean одинаково ненадёжны. Разработчики выпускают обновления, устраняющие ошибки ядра и повышающие устойчивость системы. В сентябре 2026 года в Lean 4.34 были исправлены несколько проблем, связанных с корректностью проверки доказательств, а последующие обновления продолжили укреплять защиту. Риски зависят от версии системы, способа проверки и того, насколько тщательно обрабатываются доказательства из недоверенных источников.

Что стоит за доверием к формальной математике

Ещё один вопрос связан с логическими основаниями Lean. Значительная часть современной математики строится на теории множеств, тогда как Lean использует теорию типов — другой формальный фундамент, позволяющий задавать математические объекты и строить доказательства.

Майло Мозес, аспирант Калифорнийского технологического института, обращает внимание на то, что теория множеств прошла длительную историю изучения и проверки математическим сообществом. Теория типов также имеет серьёзную математическую основу, однако для некоторых исследователей важен вопрос о том, как её согласованность соотносится с другими формальными основаниями математики.

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

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

По словам Энн Баанен, участвующей в сопровождении Mathlib, надёжность и качество формализаций остаются важными условиями включения новых результатов в библиотеку.

От математических ошибок к безопасности ИИ

Значение формальной верификации выходит за пределы чистой математики. Подобные методы применяются в информатике, криптографии и разработке систем безопасности, где необходимо строго обосновывать свойства программного обеспечения.

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

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

Тем не менее общий принцип остаётся неизменным: формальная верификация полезна ровно настолько, насколько надёжны её логические основания, программная реализация и соответствие проверяемой модели реальной системе.

Кто будет проверять доказательства, созданные ИИ?

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

Для части сообщества Lean это означает утрату привычного исследовательского процесса, в котором математики совместно разбирали доказательства, обсуждали трудные места и постепенно добивались понимания результата. Если основная работа по формализации будет выполняться ИИ, роль человека может сместиться от построения доказательства к проверке того, что именно доказала машина.

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

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

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