https://openai.com/index/navier-stokes-solution/
Считать задачу однозначно решённой пока рано, публикации всего день, и независимого консенсуса математиков, что проблема решена, пока нет.
В репозитории на GitHub опубликована формализация задачи и решение в Lean — инструменте для формальной верификации. Основных вариантов, куда могла закрасться ошибка, два.
1⃣ Во-первых, это корректность формализации условия задачи. Тут OpenAI взяла уже существующую формализацию для контрпримеров C и D из проекта Google DeepMind
formal-conjectures. Впрочем, миссформализация здесь все ещё возможна, и именно ее отсутствие сейчас придется доказать кожаным.2⃣ Во-вторых, это корректность самого процесса верификации. Например, совсем недавно в Lean нашли баг, позволяющий показать принять ложное доказательство, баг исправлен в версии 4.32.2. OpenAI использует версию 4.34.0-rc2. Также в конфигурации используется параметр
"enable_nanoda": true, то есть пруф должен приниматься не только стандартным ядром Lean, но и nanoda, независимой реализацией этого ядра на Rust (кстати, тот самый баг затрагивал только классическую реализацию). То есть OpenAI следует золотым стандартам и использует связку Comparator + внешние чекеры, что в том числе защищает от наличия бага в одной из имплементаций ядра.