OpenAI 6. října zveřejnilo matematické rukopisy vytvořené neveřejným modelem. Veřejný repozitář upozorňuje na různý stav ověření a možné chyby. Nejde o vydání nového modelu pro uživatele ani o soubor výsledků, které už Neudyne odborně potvrdilo.
K části práce jsou dostupné formalizace v Lean, které umožňují počítačovou kontrolu přesně zapsaného tvrzení. To není totéž jako potvrzení každé formulace v doprovodném textu. Návod k sestavení knihovny existuje; my jsme důkazy nekompilovali. Důležitější než působivý počet souborů je shoda mezi tím, co rukopis tvrdí, a tím, co kontrolní artefakt skutečně pokrývá.
Nezávislá poradní skupina AGMAI požaduje srozumitelné vysvětlení a odpovědnost lidí za matematický obsah. Konzultace s ní proto není razítkem správnosti. Představme si užitečnější výsledek než titulek o zázračném stroji: matematik dostane nový nápad, najde slabé místo a vznikne postup, který lze bezpečně použít v další práci.
Pokud se takové postupy osvědčí, mohly by pomáhat při odvozování mezí optimalizačních algoritmů nebo při přípravě formálně kontrolovaných softwarových komponent. To je naše realistická možnost využití, nikoli doložená aplikace této kolekce. Nejdříve je nutné prověřit předpoklady, návaznost na literaturu a samotný důkaz; pak se teprve ukáže, zda je výsledek prakticky užitečný.
Optimistický redakční odhad je 4–12 týdnů pro první zveřejněné odborné rozbory vybraných tvrzení, pokud se jim budou věnovat příslušní specialisté. Přijetí celé kolekce nebo její přenos do výrobků takto datovat nelze. Skutečnou atrakcí není rychlost oznámení, ale možnost, aby objev obstál i před někým jiným než před svým autorem.
Diskusi můžete otevřít prvním komentářem.