Jedna položka v dnešním přehledu TLDR AI mi zastavila scrollování mnohem spolehlivěji než další generátor obrázků: interní systém OpenAI má vyřešit problém existence a hladkosti Navierových–Stokesových rovnic. Jestli je to správně, nejde o běžné „AI dosáhla pěkného skóre v benchmarku“, ale o věc, kterou budou muset velmi pečlivě číst matematici.
Problém, který odolával skoro sto let
Navierovy–Stokesovy rovnice popisují proudění tekutin a plynů. Patří sem voda v potrubí, vzduch kolem letadla i kouř, který se mi pokaždé záhadně rozhodne jít přímo do očí. Obtížná je hlavně jejich trojrozměrná podoba: matematici dosud nemají obecný důkaz, zda se z hladkého počátečního proudění vždy vyvine řešení, které zůstane hladké, nebo zda se v konečném čase objeví singularita.
Singularita zde zjednodušeně znamená bod, kde se matematický popis „utrhne“ a některá veličina přestane být konečná a rozumně ovladatelná. Neznamená to automaticky, že v kuchyni exploduje hrnec s polévkou; jde o zásadní otázku, zda rovnice ve 3D mají za všech okolností dobře vychované řešení.
Jde o jeden ze sedmi Millennium Prize Problems, tedy problémů, za jejichž vyřešení Clay Mathematics Institute vypsal cenu milion dolarů. Jeden z nich, Poincarého domněnka, už vyřešen byl. Zbytek má pověst úloh, u kterých si i velmi schopný člověk může připadat jako já při pokusu pochopit první odstavec odborného článku.
Co má systém OpenAI konkrétně udělat
TLDR AI uvádí, že systém ukázal vznik singularity v konečném čase u hladké trojrozměrné dynamiky tekutin. Součástí výsledku má být analytický důkaz, tedy důkaz napsaný v běžném matematickém aparátu, a také formalizace v Lean.
Lean je proof assistant, program určený k přesnému zápisu matematických definic a kontrole jednotlivých kroků důkazu. Neověřuje, že je nápad důkazu zajímavý nebo že člověk správně pochopil zadání; umí ale zkontrolovat, zda na sebe formálně navazují kroky, které mu zadáte. U takhle citlivého tvrzení je to velmi cenná pojistka proti nenápadné chybě v logice.
Současně bych z formalizace nedělala automatickou pečeť „vyřešeno“. Záleží na tom, co přesně Lean obsahuje: zda je ve formálním zápisu celý argument, jaké používá předpoklady a zda ty opravdu odpovídají původnímu problému. To jsou otázky pro odborníky na parciální diferenciální rovnice i formální verifikaci, ne pro nadšenou blogerku s otevřenými pěti záložkami.
Největší háček: chybí samotný důkaz
Podklad mluví o oznámení OpenAI, ale neobsahuje odkaz na odborný text, repozitář Lean formalizace ani vyjádření nezávislých matematiků. Z něj proto neplyne, jak důkaz vypadá, kdo jej kontroloval ani zda už začalo odborné posuzování. A právě tady se bude rozhodovat, jestli jde o historickou matematickou zprávu, nebo o velmi ambiciózní tvrzení, které se ještě rozebere na prvočinitele.
Mně osobně přijde zajímavé už to, že se u podobného výsledku zmiňuje vedle analytického důkazu i Lean. AI systémy bývají dobré v hledání vzorců a navrhování postupů, jenže matematika si právem potrpí na to, aby každý most přes propast opravdu držel. Kombinace nápadu stroje, lidského ověření a formální kontroly by mohla být praktičtější než hledat jednu magickou AI, která všechno vyřeší sama.
Počkejme si na čtení, ne na titulky
Pokud se výsledek potvrdí, bude to silný argument, že AI může přispět i k dlouhodobému základnímu výzkumu, ne jen urychlit rutinní práci. Zatím ale beru zprávu jako důvod zbystřit, nikoli jako důvod přepisovat učebnice.
Nejraději bych teď viděla veřejný důkaz, jeho Lean verzi a reakce lidí, kteří Navierovy–Stokesovy rovnice studují celý profesní život. Titulek je skvělý začátek; matematický konsenzus je ta podstatně těžší část.
