OpenAI zveřejnilo řešení slavného problému Navierových–Stokesových rovnic
OpenAI představilo řešení problému Navierových–Stokesových rovnic, který patří mezi takzvané problémy tisíciletí. Součástí zveřejněného materiálu je textové pojednání i formální důkaz zapsaný v jazyce Lean.
Řešení zveřejněné OpenAI
OpenAI oznámilo, že zveřejňuje řešení matematického problému Navierových–Stokesových rovnic. Jde o úlohu označovanou jako problém tisíciletí, což je přímo součást názvu materiálu, který společnost publikovala.
Z dostupného shrnutí není zřejmé, jaký přesný postup autoři při řešení použili ani k jakému konkrétnímu závěru dospěli. OpenAI pouze uvádí, že sdílí řešení tohoto problému vytvořené umělou inteligencí.
Dvě části materiálu
Zveřejněný materiál má podle OpenAI dvě hlavní podoby. První představuje samotný písemný výklad řešení, tedy text, který má popisovat postup a výsledek práce.
Druhou částí je formální důkaz zapsaný v jazyce Lean. Ten se od běžného matematického textu liší tím, že je určen k přesnému formalizovanému zápisu důkazu. Podklad však neuvádí jeho rozsah ani podrobnosti.
Co lze říct s jistotou
Z krátkého oznámení nelze vyvozovat, že byl problém definitivně uznán matematickou komunitou nebo že řešení splňuje všechny podmínky spojené s takzvanou cenou tisíciletí. OpenAI v dostupném shrnutí pouze popisuje zveřejněný materiál jako řešení a zmiňuje jeho formální podobu v Leanu.
Stejně tak nejsou k dispozici informace o tom, jakou roli při vzniku důkazu sehrála umělá inteligence nebo kdo práci kontroloval.
Význam formalizovaného důkazu
Zahrnutí důkazu v Leanu ukazuje na snahu popsat matematické řešení způsobem vhodným pro formální ověřování. Samotné zveřejnění ale podle dostupného podkladu neposkytuje další podrobnosti o výsledcích ani o procesu kontroly.
Pro posouzení významu oznámení bude proto nutné vycházet z úplného textu řešení a z formálního důkazu, nikoli pouze z krátkého RSS shrnutí. To samo potvrzuje jen to, že OpenAI oba materiály sdílí.