Як я намагався штурмувати P vs NP разом з Claude — і чому «код компілюється» це ще не «доведено»

💡 Усі статті, обговорення, новини про AI — в одному місці. Приєднуйтесь до AI спільноти!

Якщо ви бодай трохи цікавилися теорією складності, то знаєте: P vs NP — це та сама задача тисячоліття, за розв’язання якої Clay Institute обіцяє мільйон доларів. Мільйони розробників у якийсь момент думали: «а що як натравити на неї LLM?» Я теж подумав.

Спойлер: P vs NP досі не розв’язана. Але в процесі стався несподівано корисний урок про те, як (не) варто довіряти ані ChatGPT/Claude, ані навіть компілятору формального доказового асистента — і цей урок актуальний для будь-кого, хто працює з ШІ в продакшн-коді, а не тільки для математиків.

Задум

Ідея була така: взяти Lean 4 — мову й доказовий асистент, у якому кожен логічний крок перевіряється машиною без жодних припущень на слово, — і спробувати формалізувати щось із Geometric Complexity Theory (GCT), одного з найперспективніших підходів до P vs NP через алгебраїчну геометрію та теорію представлень груп.

Спойлер номер два: за кілька сесій з Claude я не наблизився до P≠NP ні на йоту. Але отримав дещо інше — маленький, чесний, повністю доведений шматочок математичної інфраструктури, і разом з ним — дуже наочний урок про природу «доведеності» в епоху ШІ-асистованої розробки.

Урок № 1: компілюється — не означає доведено

Перший файл, який ми з Claude написали, компілювався без жодної помилки. Теорема з назвою на кшталт VP_ne_VNP_target виводилась... з трьох аксіом (axiom у Lean — це твердження, яке приймається без доведення, «повірте на слово»). Формально Lean не бреше — він каже: «якщо прийняти ці три постулати, то ось цей висновок логічно з них випливає». Але самі постулати ми просто задекларували, не довівши.

Це як написати unit-тест, який мокає всю бізнес-логіку, а тоді перевіряє, що мок повертає те, що ти в нього і поклав. Тест зелений. Це нічого не означає.

У Lean є команда, яка рятує: #print axioms your_theorem. Вона показує повний список аксіом, на які спирається доведення. Якщо там тільки propext, Classical.choice, Quot.sound — це стандартна логіка самого Lean, все чисто. Якщо там з’являється щось із назвою типу irrepMultiplicity_semicontinuous — це ваша власна, недоведена аксіома, і весь «результат» тримається на довірі до неї.

Ми чесно прогнали #print axioms і побачили: 3 змістовні аксіоми, 0 реальних доведень. Синтаксична коректність, нуль математичного прогресу. Це стало правилом на весь подальший проєкт: жодна теорема не рахується «зробленою», доки #print axioms не покаже чистий список.

Ось як це виглядало в коді. Спочатку — сама «діра», замаскована під респектабельний математичний факт:

-- Постулюємо ключовий факт "на віру" — ось де живе вся дірка
axiom irrepMultiplicity_semicontinuous
    (f g : PolyRing m) (lam : Partition)
    (h : g ∈ orbitClosure m A f) :
    multiplicity m g lam ≤ multiplicity m f lam

-- А ця теорема виглядає солідно, і компілюється без жодної помилки...
theorem VP_ne_VNP_target
    (n c : ℕ) (m : ℕ) (hm : m ≤ n ^ c) (f g : PolyRing m) (lam : Partition)
    (hpos : 0 < multiplicity m f lam) (hzero : multiplicity m g lam = 0) :
    f ∉ orbitClosure m A g :=
  separation_from_obstruction m A f g lam hpos hzero

...і ось команда, яка миттєво знімає ілюзію:

#print axioms VP_ne_VNP_target
-- [VP_ne_VNP_target] depends on axioms:
--   [irrepMultiplicity_semicontinuous, irrepMultiplicity, zariski_topology,
--    propext, Classical.choice, Quot.sound]

Перші три рядки виводу — наші власні, недоведені постулати. Останні три — стандартна логіка Lean, з ними все гаразд. Правило просте: якщо у виводі #print axioms є щось, крім propext, Classical.choice і Quot.sound, — перед вами не доведення, а домовленість вірити на слово.

Урок № 2: навіть ШІ-асистент помиляється в арифметиці — рахуйте вручну

Ми звузили амбіції до чогось реально доказового: hook length formula — класичної формули з комбінаторики теорії представлень, яка обчислює розмірність незвідних представлень симетричної групи Sₙ через «діаграми Юнга» (візуальне представлення розбиття числа на клітинки) і «крюки» — довжини специфічних куточків цих діаграм.

У якийсь момент Claude вивів формулу для конкретного класу діаграм (так званий hook shape) і помилився: замість правильної відповіді C(2k,k) видав просто k. Виглядало правдоподібно, компілятор би це навіть не спіймав (це arithmetic твердження, яке ще не було закодоване) — але ручна перевірка на маленькому прикладі (k=1, S₃) одразу показала розбіжність: k=1 давало відповідь 1, а правильна відповідь мала бути 2.

От як виглядала ручна перевірка на найменшому нетривіальному прикладі — діаграма λ=(2,1), тобто k=1:

Добуток крюків = 3·1·1 = 3. Розмірність = n!/добуток = 3!/3 = 2. Формула Claude (k) для k=1 давала 1 — розбіжність одразу видно на найпростішому прикладі, ще до написання загального доведення.

Мораль: ШІ чудово генерує правдоподібний текст і код, включно з математичними твердженнями, які звучать переконливо. Єдиний надійний спосіб перевірки — незалежний перерахунок на маленькому конкретному прикладі, перш ніж кодувати загальний випадок. Це стосується не лише формальної математики — та сама логіка застосовна до будь-якого ШІ-згенерованого коду з нетривіальною логікою.

Що реально вдалося довести

Зрештою в проєкті github.com/illyar80/p_vs_np з’явилося:

• Формула крюків для «hook shapes» (діаграм виду одна довга перша строка + стовпчик під нею) — повністю доведена, нуль sorry (заглушок «доведу пізніше»), нуль змістовних аксіом.
• Формула крюків для двострокових діаграм — те саме, плюс вихід на класичну «ballot number formula».
• Формальний міст між нашим власним представленням діаграм і вбудованою структурою YoungDiagram з Mathlib (стандартна математична бібліотека для Lean) — щоб довести, що обидва підходи рахують одне й те саме.
• Комбінаторна оцінка (частина A програми Bürgisser—Ikenmeyer—Panova) — теж повністю доведена.
• І чесно позначена відкрита частина: повна no-go теорема BIP вимагає результатів з теорії коефіцієнтів Кронекера, які на сьогодні — нерозв’язана дослідницька задача світового рівня. Ми це не приховали під sorry, а просто не стали формалізовувати, чітко описавши в README, чого бракує і чому.

Підсумковий стан проєкту виглядає так:

Важливо чесно сказати: сама загальна формула крюків (для будь-якої діаграми Юнга) вже була доведена в Lean раніше іншим автором, іншим методом (імовірнісний «hook walk»). Наш внесок — незалежна перевірка іншим, елементарним методом для двох конкретних сімейств, плюс явні замкнуті формули та міст до стандартної бібліотеки. Це скромний, але чесний результат — і я свідомо не називаю це «проривом» чи «заповненням прогалини», бо це неправда.

Найкраща частина: як швидко ловлять брехню

Десь посеред роботи над проєктом мені трапився свіжий (червень 2026) препринт на arXiv: T.S. Артанарі заявив повне машинно-верифіковане в Lean 4 доведення P = NP через зведення симетричної задачі комівояжера до поліедральної membership problem. Стаття містила фрази на кшталт «Lean 4 rejects any gap... there is no possibility of a subtle error slipping through» і статистику «2968/2968 build targets clean».

Звучить переконливо, правда? Компілюється без помилок, нуль sorry в основному ланцюжку доведення.

За один день хтось відкрив у репозиторії Issue з назвою «Main theorem currently proves True, not P = NP». З’ясувалося: ключове визначення виглядало приблизно так:

-- Ось і вся "історична теорема P = NP":
def P_equals_NP : Prop := True
def SAT_in_P : Prop := True

theorem p_equals_np (n : ℕ) (hn : 5 ≤ n) : P_equals_NP := by
  trivial  -- ще б пак, це ж просто True

Теорема доводила «True = True» — тавтологію, яка ніяк не відповідала заявленому змісту. Компілятор це, звісно, пропустив: з погляду Lean, True — цілком коректний тип, і довести True — тривіально (trivial закриває будь-яку ціль True миттєво). Але саме твердження було підмінене на порожнє ще на етапі формулювання, до будь-якого доведення. «2968/2968 build targets clean» — і жодного стосунку до реальної проблеми P vs NP.

Це і є справжня мораль усієї цієї подорожі, актуальна для будь-кого, хто працює з формальними методами, тестами чи ШІ-згенерованим кодом: компілятор (чи test suite, чи CI) перевіряє внутрішню узгодженість відносно того, що ви йому сформулювали — а не те, чи ваше формулювання відповідає реальності. Помилка може ховатися не в логіці виведення, а в самій постановці задачі — і жоден зелений білд це не зловить.

Практичні висновки для розробників

Навіть якщо ви ніколи не відкриєте Lean:

1. «Тести проходять» і «код працює правильно» — різні твердження. Завжди питайте: а що саме перевіряє цей тест? Чи не замокано випадково саму суть перевірки?
2. ШІ-асистенти чудово генерують правдоподібні, синтаксично бездоганні артефакти — включно з тестами, доведеннями, специфікаціями — які можуть бути змістовно порожніми. Перевіряйте на маленьких конкретних прикладах вручну, перш ніж довіряти узагальненню.
3. Явно розділяйте «доведено», «допущено на віру» (аксіома/mock/TODO) і «відкрито» — і в коді, і в документації. Наш README прямо перелічує, що саме доведено, що спирається на власні недоведені аксіоми, а що — чесно позначена нерозв’язана задача. Ця прозорість коштує дешево і рятує від пізнішого сорому.
4. Якщо цікаво копнути глибше в саму математику — почніть з класичного огляду Скотта Ааронсона «P =? NP» (є у вільному доступі), а живі обговорення свіжих заявлених доведень шукайте на cstheory.stackexchange.com.

P vs NP, найімовірніше, не впаде найближчим часом ні від рук ШІ, ні від рук людини поодинці. Але дисципліна «довіряй, та перевіряй — на маленькому прикладі, руками» виявилась куди ціннішим сувеніром з цієї подорожі, ніж будь-яка окрема лема про довжини крюків.