OpenAI a 370 matematických problémů: co je ověřené a kde čeká marketing

OpenAI tvrdí, že jeho průkopnický model přispěl k řešení nebo rozkladu více než 370 matematických problémů. Číslo vyvolalo jeden z největších mediálních ohlasů v historii matematiky. Zveřejněné podklady však zatím nepotvrzují správnost všech výsledků.

Čím přesně model přispěl? Které výsledky prošly odbornou kontrolou? A kde začíná marketing? Právě na těchto otázkách záleží, zda 370 znamená skutečný posun, nebo součet výsledků s různou důkazní hodnotou.

OpenAI zveřejnilo repozitář s Leanovými formalizacemi, pravidla pro revize, citování a další podklady. Samotné oznámení ale neobsahuje seznam všech problémů ani jednotlivé důkazy. Neuvádí také nezávislé potvrzení jejich správnosti.

Co přesně OpenAI tvrdí

Rozsah tvrzení není jednolitý. Některé příspěvky mohou představovat nové důkazy, jiné rozklad problému nebo výsledky, které v době vzniku ještě nebyly přijaty jako nové.

„Vyřešeno 370 problémů“ proto není totéž jako „370 nových originálních důkazů“. Čtenář potřebuje vědět, s jakým typem výsledku se setkává a jakou míru kontroly má.

OpenAI zároveň zdůrazňuje transparentnost. Ke sdíleným podkladům patří shrnutí uvažování modelu, odhady výpočetních nákladů a statistiky pokusů.

Průměrný výsledek prý vyžádal výpočetní prostředky odpovídající přibližně třem hodinám přemýšlení ChatGPT Pro. Jde o přepočet na běžnou uživatelskou jednotku, nikoli o nezávisle změřený výpočet na veřejné infrastruktuře.

Diskutující se proto shodují spíše na principu než na konkrétním čísle. Někteří považují výsledky za významný posun, jiní varují před přenesením firemního marketingu do médií. Všem ale záleží na nezávislé kontrole.

Pro čtenáře je zásadní rozlišit čtyři stavy:

• strojově ověřený důkaz,
• Leanová formalizace bez odborné revize,
• pouze textový rukopis,
• stažený příklad.

Tyto výsledky nelze směšovat do jednoho průměru.

Jak se výsledky ověřovaly

Odborný postup má zhruba tři vrstvy.

Nejprve přichází matematická kontrola. Odborník porovná výsledek se zadáním a prověří definice, předpoklady i případné mezikroky.

Druhou vrstvou je strojová kontrola formálního zápisu v Leanu. Třetí je nezávislá reprodukce. Při ní se výsledek ověřuje z otevřených podkladů, ideálně bez přístupu k internímu modelu.

Lean 4 s knihovnou mathlib je vhodným nástrojem pro strojově kontrolovaný důkaz. Repozitář je potřeba sestavit čistě, bez placeholderů a bez neočekávaných axiomů.

Kde byly silnější knihovny, může dávat smysl alternativa, například Isabelle/HOL nebo Rocq. AlphaProof se používá k agentnímu hledání důkazních taktik, nikoli jako náhrada lidské revize.

LIVE TEST SCREENSHOT

Jak to funguje pod kapotou a kde má postup limity

Přesný odborný název postupu je počítačem podporovaná formální verifikace matematického důkazu. Diskuze často mluví jednoduše o „důkazu v Leanu“. To zní, jako by samotný formalizovaný kód dokazoval matematické tvrzení.

Ve skutečnosti jde o systém návrh–překlad–kontrola: model navrhne lemma nebo konstrukci, autoformalizátor je přepíše do Leanu a kernel rozhodne, zda přijme jednotlivý krok.

Odměna za přijatý krok je binární. Kernel potvrzuje, že kód odpovídá zadané formální teorii. Neověřuje však, že výrok odpovídá původnímu matematickému zadání.

Při posunu definic, kvantifikátorů nebo modelu výpočtu může certifikovat slabší nebo jiný výrok, než jaký tvrdí článek. Formální kontrola proto neřeší chybně nebo nejednoznačně formulovaný problém.

Dalším limitem je uzavřenost procesu. Bez přístupu k promptům, neúspěšným pokusům a internímu modelu nelze spolehlivě rozhodnout, zda model objevil nové řešení, nebo složil známý argument z korpusu.

Jde o variantu problému „Erdős“. Údajně nový důkaz může již existovat v literatuře. Novost proto vyžaduje samostatné srovnání s odbornými pracemi.

Metrika „hodiny přemýšlení ChatGPT Pro“ navíc směšuje výsledky s různou důkazní hodnotou do jednoho čísla. Tento přepočet usnadňuje marketingové vyjádření. Neříká ale nic o tom, kolik lidské revize výsledek potřeboval.

Kde je hranice mezi pokrokem a nadsazením

Skutečným přínosem je možnost rychle připravit kontrolovatelný formální artefakt a zvýšit přesnost matematické práce. Komunitní know-how spočívá v rozlišování jednotlivých úrovní důkazu, nikoli v prostém počítání vyřešených úloh.

Označení za „průlom“ je oprávněné teprve tehdy, když lze určit konkrétní výsledek, jeho význam a stav nezávislé revize. Samotný počet problémů, úspěšný Lean build nebo titulek o „dni v historii matematiky“ nestačí.

Dopady na výzkum jsou reálné už teď. AI může urychlit formulaci a kontrolu důkazů. Ve vzdělání však přináší riziko: student může přijmout chybnou konstrukci jen proto, že prošla automatickou kontrolou.

Důležité je proto učit rozlišovat zadání, draft, formální důkaz a publikovaný výsledek. Každá fáze má jinou míru jistoty.

Dostupnost modelů je druhá významná otázka. Výkonné systémy mohou zůstat omezené na instituce a firmy, které mají výpočetní kapacitu i odborné týmy.

To by posílilo rozdíl mezi těmi, kdo mohou AI používat jako nástroj průzkumu, a těmi, kdo ji musí zveřejňovat nebo obhajovat.

Co si z toho vzít

• „370 vyřešených problémů“ není jednotné měřítko. Rozlišujte nové důkazy, rozklady, rukopisy a Lean-checked výsledky.
• Formální kontrola ověřuje kód v dané teorii, nikoli automaticky původní matematické tvrzení.
• Nezávislá reprodukce vyžaduje otevřené podklady, čisté sestavení repozitáře a revizi bez skrytých axiomů.
• Novost výsledku je samostatná otázka; vyžaduje srovnání s literaturou.
• Pro práci s důkazy je GPT-6 Pro užitečný jako podpora při formulaci a revizi, ne jako autorita, která nahrazuje kontrolu.
• Ověřování faktů pomocí AI a AI Governance se týkají nejen modelů, ale také přístupu k výpočtům, transparentnosti a odpovědnosti za výsledky.