Нав'є–Стокс і доведення в Lean: вимушені особливості та непрозорість лабораторії

8 вересня 2026 року OpenAI заявила, що її внутрішня модель, яку ніколи не поширювали публічно, отримала доведення вибуху за скінченний час для тривимірних нестисливих рівнянь Нав'є–Стокса. Компанія оприлюднила теоретичний документ і відкритий репозиторій NavierStokesAndEuler, що містить формалізацію мовою Lean 4 теорем про гладкі початкові дані під дією зовнішнього вимушувального члена. За викладом самої лабораторії, результат покриває твердження про втрату регулярності з формулювання, укладеного математиком Чарльзом Фефферманом для Інституту Клея, проте не торкається випадку без зовнішньої сили, який наукова спільнота вважає складнішим варіантом задачі. Автор офіційного формулювання назвав розв'язання захопливим, згадавши внесок Кордоби та Мартінеса-Сороа, тоді як компанія від початку пояснила, що не має наміру претендувати на приз в один мільйон доларів.

Ця історія переплітає автоматизацію математики з ритмом академічних інституцій. Інститут Клея й далі тримає Нав'є–Стокса серед нерозв'язаних задач: регламент вимагає публікації у кваліфікованому виданні, витримки щонайменше два роки від публікації та загального визнання математичною спільнотою, а по суті інститут досі не висловився. Його президент Мартін Бридсон нагадав, що оцінювання свідомо йде неквапливим темпом, аби гарантувати цілковиту строгість. Картину ускладнює суперечка про пріоритет із паралельною працею, яку виклав математик Теренс Тао і яку самі автори описують як значною мірою виконану за допомогою штучного інтелекту. Математик із Нью-Йоркського університету заперечив надану лабораторією версію контактів, припустивши, що до результату могли долучитися приватні сесії з пропрієтарним інструментом; компанія заперечує, що бачила неопубліковану роботу безпосередньо, хоч і визнає, що не може виключити впливу знеособлених даних використання на навчання власних моделей.

У репозиторії наведено інструкції, щоб доведення перевірила машина, але жодної завершеної незалежної перевірки досі немає; поза цією перевіркою пропрієтарна природа використаної інфраструктури унеможливлює будь-яку незалежну перевірку витрат і виставлених напоказ показників ефективності. Заявлені обчислення — близько десяти тисяч одночасних агентів між 1 і 5 вересня, 88 годин до отримання доведення і ще 17 на формалізацію та перевірку в Lean — лишаються корпоративними твердженнями, яких ззовні ніхто не відтворить. Без доступу до навчального коду чи до ваг системи наукова спільнота може підтвердити лише формальні кроки, викладені в репозиторії, а справжні умови відтворюваності експерименту залишаються в тіні.

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

— Olya