Математики нашли несоответствие в доказательстве ИИ OpenAI одной из задач тысячелетия.
Математики нашли несоответствие в доказательстве ИИ одной из задач тысячелетия.
Исследователи обнаружили ошибку в компьютерной версии доказательства, с помощью которого ИИ OpenAI заявил о решении задачи Навье-Стокса, одной из самых сложных проблем современной математики. При переводе доказательства в язык Lean одна из формул изменилась: вместо условия, что величина меньше m+4, в коде оказалось условие, что она меньше m+5. Это более слабое ограничение, которое не полностью соответствует исходному тексту.
Мы подчеркиваем: ошибка не означает, что исходное доказательство обязательно неверно. Однако этот случай показывает, что даже если компьютерный код формально проходит проверку, это еще не гарантирует, что он точно отражает математическую аргументацию. Ученым по-прежнему необходимо тщательно проверять результаты, созданные ИИ.

