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