OpenAI заявила про розв’язання задачі Нав’є—Стокса: що відомо

Що означають зовнішня сила, перевірка в Lean та правила премії Clay — і як оцінювати гучну математичну заяву.

Абстрактний блакитний вихор із тонкими бурштиновими нитками на темно-синьому тлі

8 вересня OpenAI заявила про розв’язання задачі Нав’є—Стокса.

Рівняння описують рух рідин і газів. Задача входить до семи задач тисячоліття Clay, для кожної з яких передбачено $1 млн. Це розмір премії, а не повідомлення про її присудження.

Що саме запропоновано

У науковій роботі OpenAI описано тривимірну течію, яка починається зі стану спокою під дією гладкої зовнішньої сили. Автори стверджують, що за скінченний час швидкість стає необмеженою, хоча кінетична енергія залишається обмеженою. Такий математичний зрив називають сингулярністю. Це конструкція всередині рівнянь: вода у фізичному експерименті не розганялася до нескінченної швидкості.

За описом авторів, центральний вихор звужується та прискорюється. Найскладніше — показати, що зовнішня сила залишається гладкою: необмежене зростання має виникати в динаміці течії, а не бути закладеним у саму силу.

У постановці Clay Mathematics Institute є чотири альтернативи. Варіанти A і B стосуються існування гладких розв’язків без зовнішньої сили; C і D допускають побудову прикладу зриву з гладкою силою. Саме C і D зазначені в новій роботі. Тому «є зовнішня сила» саме по собі не означає невідповідності умовам премії. Водночас такий результат не встановлює зрив для випадку без зовнішньої сили.

Роль моделей

OpenAI уточнює: доведення шукала внутрішня модель, потужніша за GPT‑6 Astra. Astra виконувала формалізацію та перевірку в Lean.

Як працює поділ завдання між програмними виконавцями, пояснюємо в матеріалі що таке AI-агенти.

Лупа над чистим аркушем паперу поруч зі структурою зі скляних і бурштинових вузлів
Логічну перевірку та відповідність постановці задачі потрібно розрізняти. Концептуальна ілюстрація.

Що дає перевірка в Lean

Lean — інструмент для формальних доведень. Він перевіряє логічний вивід із визначень, попередніх теорем та аксіом. Це дозволяє оцінювати доведення незалежно від переконливості тексту, який згенерувала модель. Водночас документація Lean окремо наголошує: коректність доведення і значення сформульованої теореми — різні питання. Потрібно також перевірити, що формальний запис відповідає початковій задачі.

OpenAI відкрила репозиторій із формалізаціями та інструкціями для їх збирання й незалежної перевірки. Це матеріали, з якими можуть працювати інші фахівці. Наявність коду не означає, що редакція RozumTech самостійно перевірила математичне доведення: такого аудиту ми не проводили.

Чи вже визнано задачу розв’язаною

Під час перевірки 9 вересня на сторінці Clay Mathematics Institute задача ще позначена як нерозв’язана. Це зафіксований стан сторінки, а не висновок інституту про помилку в роботі.

OpenAI зазначає, що не планує претендувати на премію.

Для розгляду премії правила Clay вимагають публікації у відповідному науковому виданні, щонайменше двох років після неї та загального визнання світовою математичною спільнотою. Цей строк стосується процедури премії; він не заважає математикам аналізувати роботу вже зараз.

Для читача головне питання — чи підтвердять фахівці відповідність доведення заявленій задачі. Обчислювальний результат такого рівня заслуговує на увагу, але його не слід перетворювати на обіцянку, що чатбот відтепер безпомилково розв’язує будь-яку наукову проблему.

Обговорення

Долучайтеся до розмови

Пишіть по суті й поважайте інших читачів. Перший коментар може з’явитися після перевірки редакцією.

Залишити коментар

Ваш email не публікується. Поля зі зірочкою обов’язкові.

Надсилаючи коментар, ви погоджуєтеся на його перевірку та зберігання введених даних відповідно до політики конфіденційності.