Доказательство OpenAI уравнений Навье-Стокса в Lean 4: математическая корректность против физической реальности

Исследователи проанализировали формальное доказательство OpenAI в Lean 4, показав, что хотя логика верна и код компилируется без ошибок, решение физически нереализуемо — жидкость испаряется на наномасштабе из-за трения. Это иллюстрирует проблему specification gaming, когда ИИ находит математически верный, но физически бессмысленный путь решения задачи. Автор предлагает добавить в нейро-символические системы третий компонент — проверку на соответствие законам физики, а не только формальной логике.