AI zverejnila stovky matematických dôkazov, kontrola sa len začína

OpenAI 6. októbra 2026 zverejnila matematické výsledky interného modelu vo verejnom repozitári GitHub spolu s formalizáciami mnohých dôkazov v systéme Lean a desiatimi skrátenými súhrnmi uvažovania modelu. Matematici majú prístup k predloženým argumentom, ich zverejnenie však samo osebe neznamená nezávislé potvrdenie výsledkov. Model, ktorý ich vytvoril, zatiaľ verejne dostupný nie je.

Pri pôvodnom súbore 722 rukopisov usporiadaných do 372 rodín výsledkov Axios citoval Stephena Wolframa slovami „You can make a trillion theorems easily“. Jeho poznámka pomenúva otázku, ktorú počet textov nevyrieši: ktoré predložené dôkazy sú správne a ktoré tvrdenia budú pre ďalší výskum dôležité? Odborné posudzovanie zbierky pokračuje.

Čo obsahuje vydaný súbor

Rukopisy opisujú výsledky pri otvorených výskumných otázkach, ktorými OpenAI hodnotila svoj interný model. Rodina združuje súvisiace práce: môže obsahovať hlavný výsledok, pomocný argument, jeho dôsledok alebo alternatívny dôkaz. Počet rukopisov preto nevyjadruje počet samostatne vyriešených otvorených problémov. Ani prítomnosť viacerých textov v jednej rodine nehovorí, koľko jej tvrdení už prešlo odbornou kontrolou.

Verejný repozitár umožňuje skúmať konkrétne znenie tvrdení a sledovať ich opravy. To je dôležité najmä tam, kde jeden argument používa výsledok z ďalšieho rukopisu: chyba v spoločnom východisku sa môže preniesť do nadväzujúcich prác. Pravidlá uchovávania starších verzií zároveň umožňujú rozlíšiť pôvodne predložený dôkaz od neskoršej opravy. Zverejnené výstupy tak poskytujú materiál na kontrolu, hoci celý postup ich vytvorenia nemožno zopakovať pomocou toho istého interného modelu.

Rukopis ešte nie je prijatý dôkaz

Prvou úrovňou je predložený rukopis: obsahuje matematické tvrdenie a argument, ktorý má ukázať jeho platnosť. Odborník musí preveriť, či jednotlivé kroky skutočne vyplývajú z predpokladov, či sú použité staršie výsledky správne citované a či záver zodpovedá presnému zneniu otázky. Pri otvorenom probléme môže zmena jedinej podmienky znamenať rozdiel medzi úplným riešením a užitočným, ale užším výsledkom.

Nezávislé posúdenie pridáva kontrolu ľudí, ktorí sa danej oblasti venujú a môžu preveriť aj súvislosti mimo samotného textu. Tí hodnotia pôvodnosť postupu, prípadné závislosti od iných rukopisov a miesto výsledku v doterajšej literatúre. Počas takejto práce sa môže ukázať, že dôkaz potrebuje doplniť, že tvrdenie platí iba pri silnejších predpokladoch alebo že podobný výsledok už bol známy. Každý z týchto záverov mení vedecký význam rukopisu iným spôsobom.

Správnosť a význam sú pritom odlišné otázky. Aj bezchybná veta môže byť pre ďalší výskum okrajová, zatiaľ čo dôkaz, ktorý otvorí nový postup alebo spojí vzdialené problémy, môže mať širší dosah. Wolframova poznámka smerovala práve k tomuto rozdielu. Rozsah vydania vzbudzuje pozornosť, hodnotu jednotlivých výsledkov však ukáže až ich odborné prijatie a následné využitie.

Čo pridáva formálna verifikácia v Leane

Lean umožňuje zapísať matematické tvrdenie a dôkaz v presnom jazyku, v ktorom počítač kontroluje odvodenie jednotlivých krokov. Ak takáto kontrola prejde, poskytuje silné potvrdenie, že formálne zapísaný záver vyplýva z použitých definícií a predpokladov. Pri rozsiahlych argumentoch môže zachytiť medzeru, ktorú by čitateľ pri bežnom zápise ľahko prehliadol. Formalizácia preto predstavuje ďalšiu úroveň kontroly nad rámec samotného rukopisu.

Rozhodujúce je však aj to, ktorá veta bola zapísaná. Počítač môže správne overiť formálny dôkaz užšieho tvrdenia, než aké čitateľ očakáva z názvu rukopisu. Matematici preto stále musia posúdiť preklad pôvodnej otázky do formálneho jazyka, význam predpokladov aj novosť výsledku. Vydaná zbierka navyše obsahuje práce v rôznych štádiách formalizácie. Prítomnosť zápisu v Leane pri časti výsledkov sa nedá preniesť na celý súbor.

Prvé opravy ukázali, prečo záleží na verzii

K 7. októbru 2026 história zmien repozitára uvádzala stiahnutie troch rukopisov po chybe znamienka v podkladovom argumente, úpravy ďalších 14 textov a formalizáciu hlavných výsledkov pri 300 zo 719 zostávajúcich rukopisov, teda približne 42 percent. Chyba zasiahla pôvodný argument aj práce, ktoré z neho vychádzali. Stiahnuté rukopisy zostali dohľadateľné s upozornením na medzeru v dôkaze.

Úpravy mali rôznu povahu: zahŕňali opravy dôkazov, spresnenia tvrdení a vysvetlenia predpokladov. Pri matematickom výsledku nie je jedno, či nová verzia mení iba výklad, alebo samotný rozsah vety. História zbierky preto umožňuje posudzovať presne tú podobu argumentu, ktorá je práve predložená. Skoré stiahnutia zároveň ukazujú, že aj chyba v jedinom podkladovom kroku môže ovplyvniť viacero súvisiacich rukopisov.

Čo môže vydanie znamenať pre výskum

Verejná zbierka sprístupnila matematikom veľký súbor návrhov, z ktorého môžu vzniknúť opravené dôkazy, nové otázky aj nadväzujúce práce. Takýto dosah sa však nedá odvodiť z počtu súborov. Záleží na tom, ktoré argumenty obstoja pri nezávislom čítaní, či formalizované vety zodpovedajú pôvodným otázkam a či výsledky prinášajú postupy použiteľné aj mimo svojho bezprostredného problému.

Ďalším konkrétnym posunom budú nové verzie jednotlivých rukopisov, ďalšie formálne zápisy a odborné posúdenia konkrétnych tvrdení. Práve pri nich sa rozhodne, ktoré z verejne predložených výsledkov sa stanú spoľahlivým východiskom pre ďalšiu matematickú prácu.

Prečítajte si aj:

• Kontrola uniknutého hesla: celé heslo nemusí opustiť prehliadač
• Google zastavil odmeny za chyby: automatické hlásenia zahltili kontrolu
• Printful či Printify: vyššia marža môže znamenať viac kontroly kvality