Když OpenAI oznámí, že její umělá inteligence vyřešila jeden z nejslavnějších problémů matematiky, je lákavé napsat, že stroje právě porazily člověka. Jenže u důkazu nestačí působivý výsledek ani stovky stran technického textu. Důležité je také přesně říct, co bylo dokázáno, z jakých předpokladů se vycházelo a kdo může výsledek nezávisle zkontrolovat. Rychlá zpráva o oznámení OpenAI proto skrývá mnohem zajímavější příběh, než jaký se vejde do titulku.
OpenAI tvrdí, že její tým s pomocí interního systému koordinovaných AI agentů vytvořil důkaz konečného času vzniku singularity v trojrozměrných Navierových–Stokesových rovnicích. Firma zveřejnila také rozsáhlý dokument s formalizovanou verzí v jazyce Lean. Současně ale matematik Tristan Buckmaster a výzkumník Levent Alpöge zveřejnili vlastní výsledky a popsali spor o to, kdy OpenAI začala na problému pracovat, co věděla o jejich postupu a komu náleží zásluhy.
Co vlastně OpenAI dokázala
Navierovy–Stokesovy rovnice popisují proudění tekutin a plynů. Používají se v matematické fyzice i při modelování jevů, které souvisejí s prouděním vzduchu, vody nebo krve. Problém není v tom, že bychom neuměli spočítat konkrétní proudění. Těžší otázka zní, zda hladké počáteční podmínky vždy zůstanou hladké, nebo zda se v konečném čase mohou vytvořit neomezeně velké rychlosti či gradienty.
Jde o jeden z problémů tisíciletí, které vypsal Clay Mathematics Institute s milionovou odměnou. Oficiální zadání Clayova institutu ale není slogan „najděte libovolnou singularitu“. Přesně stanovuje, jaké rovnice, prostory, počáteční podmínky a druh regularity musí řešení splňovat. Právě tady začíná rozdíl mezi titulkem o vyřešeném problému a matematickým tvrzením, které lze skutečně posoudit.
V dokumentu zveřejněném OpenAI autoři konstruují hladkou vnější sílu s kompaktní podporou a řešení, které začíná z klidu, ale před konečným časem má neomezenou maximální rychlost. Důležitá část je, že jde o problém s vynucením – tedy s externí silou působící v rovnici. OpenAI tvrdí, že tím naplňuje jednu z alternativ formulace problému podle Feffermana. To je konkrétnější a užší výrok než prosté tvrzení, že AI vyřešila veškerou regularitu nevnuceného proudění.
Samo o sobě to neznamená, že je výsledek chybný. Znamená to, že o něm musíme mluvit přesně. V matematice může být významný i důkaz speciální varianty problému, ale čtenář by měl vědět, zda jde o definitivní vyřešení původní otázky, nebo o konstrukci, která uzavírá jednu z jejích přesně definovaných větví.
Lean kontroluje zápis, ne historický příběh
OpenAI zdůrazňuje, že důkaz prošel formalizací v Leanu. To je důležitá pojistka: Lean umí zkontrolovat, zda jednotlivé kroky odpovídají formálním pravidlům systému a zda závěr plyne z uvedených předpokladů. Neumí ale sám rozhodnout, jestli formalizované tvrzení odpovídá tomu, co si autoři mysleli, že dokazují, ani jestli zvolený problém představuje přesně tu otázku, kterou veřejnost slyší v titulku.
Podobný rozdíl je vidět i u registru Palomar, který má pomáhat třídit matematické důkazy ověřené v Leanu. Formální kontrola řeší jednu vrstvu důvěry: zda kód projde typovým systémem a zda se v něm neskrývá nepovolený předpoklad. Lidská matematická kontrola řeší další vrstvy – zda je tvrzení relevantní, zda jsou definice použité správně a zda výsledek opravdu odpovídá problému, který měl být vyřešen.
Je to podobné jako u programu, který projde testy. To je dobrá zpráva, ale ještě to neříká, zda testy pokrývají skutečné použití, zda zadání neobsahuje chybu a zda program řeší správný problém. U matematického důkazu je tato otázka ještě citlivější, protože malá změna v předpokladech může změnit celý význam výsledku.
Spor nezačal u rovnic, ale u prvenství
Buckmaster a Alpöge ve svém veřejném prohlášení uvádějí, že pracovali na výsledcích týkajících se konečného vzniku singularit u několika příbuzných rovnic. Základní směr podle Buckmastera nevymysleli oni, ale navazovali na dřívější práci Diega Córdoby a Luise Martíneze-Zoroy. Jazykové modely podle něj pomohly posunout tento program k novým výsledkům a k formalizaci, nikoli však nahradit původní matematické myšlenky.
Jejich prohlášení zároveň popisuje schůzky s lidmi z OpenAI. Buckmaster tvrdí, že se dozvěděl o snaze OpenAI řešit podobnou cestu krátce poté, co se informace o práci dvojice dostaly k firmě. Popisuje také návrhy týkající se pořadí zveřejnění a autorství. Zároveň výslovně uvádí, že OpenAI důkaz neviděl a neví, zda byla jejich data použita.
To jsou závažná tvrzení, ale pořád jde o tvrzení jedné strany sporu. TechCrunch popsal chronologii a reakce obou stran a WIRED shrnul veřejné vyjádření OpenAI. OpenAI odmítá, že by její výzkumníci nebo agenti před zveřejněním viděli práci dvojice. Současně ale připouští, že nelze zcela vyloučit, že anonymizovaná data z používání jejích produktů mohla někdy zlepšovat modely.
Tady se oddělují tři otázky, které se v rychlých zprávách snadno slijí do jedné. První je, zda je nový důkaz matematicky správný. Druhá je, zda skutečně řeší deklarovanou variantu problému. Třetí je, kdo měl k jakým informacím přístup a jak se mají připsat zásluhy. Lean může výrazně pomoci s první otázkou, ale sám nevyřeší druhou ani třetí.
AI mění i pravidla pro připsání zásluh
Dříve bylo možné pracovní postup rekonstruovat především z poznámek, preprintu, e-mailů a historie spolupráce. U AI-assisted matematiky přibývá další vrstva: prompty, logy modelů, verze nástrojů, tréninková data a informace o tom, zda se výstupy uživatelů používají k dalšímu učení. Bez jasných pravidel může vzniknout situace, v níž dva týmy dospějí ke stejnému nápadu a nikdo nebude schopen přesvědčivě ukázat, kdo koho ovlivnil.
Neznamená to, že každý matematický text vytvořený s pomocí modelu je podezřelý. Znamená to, že vědecké instituce budou muset chtít podrobnější auditní stopu než dosud. U velkých laboratoří by mělo být běžné uvést, kdy byl problém zadán, jaké lidské zásahy následovaly, jaké modely byly použity a jak bylo vyloučeno využití neveřejných uživatelských dat.
Zajímavý kontrast nabízí formalizace Fermatovy poslední věty pomocí Claude. Tam je dobře vidět, že AI může dramaticky zkrátit převod existujícího matematického argumentu do formálního kódu, aniž by sama od nuly objevila původní větu. U Navierových–Stokesových rovnic je hranice mezi nalezením nové konstrukce, rozvinutím staršího programu a mechanickou formalizací mnohem důležitější než marketingová věta o autonomním objevu.
Nejdřív ověřit důkaz, potom psát dějiny
Nejrozumnější reakce proto není ani okamžité oslavování, ani automatické odmítnutí. Odborníci musí posoudit přesné znění věty, návaznost na předchozí práci, použité předpoklady a kvalitu formalizace. Teprve potom půjde říct, zda OpenAI uzavřela jednu z alternativ problému, nebo zda její oznámení používá širší slovo „řešení“, než jaké odpovídá matematickému obsahu.
Spor o prvenství může mezitím zastínit samotný vědecký posun. To by byla škoda. I kdyby se později ukázalo, že některá část oznámení potřebuje opravu, už nyní je zřejmé, že AI dokáže pomáhat s matematickými konstrukcemi, hledáním cest a formalizací v měřítku, které ještě nedávno působilo neprakticky.
Zároveň ale platí nepříjemná věta, kterou bude nutné opakovat častěji: formální důkaz neověřuje automaticky celý příběh kolem něj. Ověřuje konkrétní zápis konkrétního tvrzení. Kdo tvrzení objevil, jaké práce mu předcházely, zda byl problém správně položený a zda se s daty zacházelo férově, zůstává úkolem lidí.
Možná tedy nesledujeme okamžik, kdy AI vyřešila matematiku. Sledujeme okamžik, kdy se matematika učí žít s nástrojem, který umí generovat důkazy rychleji, než je komunita stačí číst, vysvětlovat a připisovat správným autorům.
