Navier–Stokes Lost in Translation
Автоматическое формализование текста из естественного языка в системы вроде Lean не гарантирует корректности исходного доказательства, даже если формальная версия проходит проверку. Проблема заключается в том, что семантически верный перевод математических утверждений из естественного языка в формальный язык требует разрешения неоднозначностей, которые формально невычислимы и находятся на самом высоком уровне иерархии вычислимой сложности (SCI = ∞), что делает задачу строго сложнее, чем проблема останова. Это означает, что никакой алгоритм, включая ИИ, не может гарантировать faithful перевод во всех случаях. На практике это приводит к ситуациям, когда формальное доказательство в Lean подтверждает что-то отличное от того, что утверждалось в естественном языке. В качестве примера авторы анализируют заявленное доказательство взрыва решений уравнений Навье–Стокса, сгенерированное ИИ и формализованное в Lean: хотя Lean-проверка проходит, формализованное утверждение не соответствует исходному естественноязычному claim, то есть доказано не то, что заявлено. Таким образом, доверие к результатам ИИ-доказательств на основе их формальной верификации вводит в заблуждение, поскольку разрыв между естественным и формальным языком остаётся фундаментальным и не преодолимым автоматическими средствами.