Matematika bývá pro AI lákavá hlavně proto, že správný důkaz by měl jít v principu ověřit. OpenAI teď ale místo několika jednotlivých úloh vysypala téměř 400 výsledků ve více než 700 rukopisech — a lidským matematikům tím nadělila práci, která může vystačit na roky.
Ne jeden důkaz, ale celý kontejner
Rozsah je na tom snad nejvíc zarážející. Materiály sahají od kombinatoriky přes geometrii, teorii čísel a algebru až po topologii, pravděpodobnost, statistickou mechaniku nebo matematickou fyziku. Už samotný obsah s abstrakty má zhruba 40 stran a několika lidem, s nimiž mluvil The Verge, zabral jeho průchod většinu hodiny.
OpenAI k repozitáři na GitHubu přidala i návod, jak se v něm pohybovat. To zní banálně, ale tady je to docela výmluvný detail: nejde o článek, který si odborník přečte u kávy a pak se pohádá o jeden krok v důkazu. Je to záplava textů, v níž je nejdřív potřeba najít, co vůbec stojí za pozornost.
Mně osobně na tom přijde fascinující i trochu tísnivé, že množství výsledků samo o sobě nemusí znamenat množství poznání. Dokud nikdo pořádně neví, které teoremy jsou nové, správné a významné, je to spíš gigantická hromada kandidátů na poznání. Velmi chytrá hromada, ale pořád hromada.
Lean pomáhá, jenže není kouzelné razítko
Část výsledků je zapsaná ve formalizačním jazyce Lean. Jde o proof assistant neboli nástroj, v němž lze důkaz zapsat tak přesně, aby jeho logickou správnost kontroloval počítač. Pro matematiku je to obrovská výhoda: člověk nemusí jen věřit, že někde v dlouhém argumentu není přehlédnutá díra.
Jenže formalizace tu není všude. Z 719 rukopisů bylo formálně zpracováno 300 hlavních výsledků, tedy přibližně 42 procent. OpenAI zároveň upozorňuje, že výsledky jsou v různých stupních ověření a další formalizace chce doplňovat později.
Ani soubor s Leanem navíc automaticky neuzavírá debatu. Matematik musí zkontrolovat, zda kód skutečně dokazuje přesně to, co tvrdí doprovodný rukopis. Někteří odborníci podle The Verge narazili na případy, kde ověřené výroky neodpovídaly úplně hladce formulacím v textu. Počítač tedy může hlídat logiku, ale člověk stále hlídá význam. A význam, potvora, se nedá odškrtnout jedním zeleným políčkem.
Obava ze slopu má tentokrát konkrétní důvod
Matematici mluvili i o takzvaném AI slopu: nekvalitním, často chybném materiálu vytvořeném AI. V akademii nejde jen o nepěkné formulace. Špatně napsaný důkaz může sežrat celé odpoledne člověku, který se snaží najít chybu, a nedostatečné citace umějí poškodit autory, na jejichž práci nová věc stojí.
OpenAI už dříve za matematické texty čelila kritice, mimo jiné kvůli slabému nebo chybějícímu uvádění zdrojů. Tentokrát jsou první dojmy některých expertů lepší, byť sami připouštějí, že laťka po minulých zkušenostech neležela zrovna v kosmu. Kevin Buzzard z Imperial College London například v oblasti algebraické teorie čísel našel řadu relevantních tvrzení, ale jen asi šest mu na první pohled vyčnívalo. U mála z nich navíc viděl okamžitě dostupné formální ověření.
To je podle mě jádro celé věci. AI možná dokáže produkovat matematické nápady rychleji, než je komunita dokáže číst. Jenže rychlost generování a rychlost důvěry nejsou totéž. Jestli se má podobný systém stát užitečným kolegou, neměl by odborníkům posílat stovky možná správných rukopisů a pak čekat, až je lidé roztřídí.
Matematici nejsou hotoví, jen dostali nový typ práce
The Verge popisuje mezi reakcemi úžas, nadšení i úzkost. Tomu rozumím. Představa, že by AI přinesla tolik ověřených a dobře vysvětlených výsledků, je nádherná. Představa, že přinese stejný počet nepřehledných textů s nejistou kvalitou, je administrativní horor v řeckých písmenech.
Zatím bych tedy nevyhlašovala, že matematiku převzaly stroje. Spíš sledujeme, zda se obor naučí žít s novým problémem: ne nedostatkem hypotéz, ale nadbytkem tvrzení, která někdo musí poctivě prověřit. A to je paradoxně velmi lidská práce.
