AI se poprvé osamostatnilo a vyřešilo 30letý matematický problém! Byla dobita poslední bastion lidstva?
V nedávno vydaném čísle časopisu Scientific American z prosince 2025, matematička Emily Riehl z Johns Hopkins University zdůraznila, že se obává, že by mohla být nahrazena umělou inteligencí (AI). Riehl v článku uvedla, že i když špičkové AI modely získávají medaile na mezinárodní matematické olympiádě, matematika si stále cení „formálních důkazů“, které odolávají logickému přezkoušení. Věří, že velké jazykové modely (LLM) dělají základní chyby a že počítačoví asistenti pro formální důkazy mají ještě dlouhou cestu k tomu, aby dosáhli standardu formální verifikace jejích výzkumných otázek. Avšak v rychle se vyvíjejícím světě AI došlo k překvapivému obratu, když AI, která má schopnost formálního dokazování, úspěšně vyřešila matematický problém, jenž visel více než 30 let.
Matematický génius: Paul Erdős
Abychom pochopili význam tohoto průlomu, je třeba se seznámit s maďarským matematikem Paulem Erdősem. Byl jedním z nejplodnějších matematiků 20. století a během svého života publikoval přibližně 1500 prací, což nikdo se svou konkurencí nikdy nedokázal překonat. Erdős žil nekonvenčně, nikdy se neoženil, neměl stálé zaměstnání ani domov; cestoval po světě s kufrem plným oblečení a zápisníků. Matematiku vnímal jako společenskou aktivitu a často se objevoval na prahu domů svých kolegů s oznámením „můj mozek je otevřen“ a poté se s nimi zapojil do intenzivní duševní debaty.
Erdős byl uznáván jako „tvůrce problémů“, během svého života formuloval tisíce nevyřešených hypotéz, nazývaných „Erdősovy problémy“. Za jejich vyřešení vypsal odměny, které se pohybovaly od 25 dolarů až po 10 000 dolarů za nejtěžší úlohy, a vyřešení Erdősových problémů bylo považováno za velký úspěch v matematickém světě.
Od spolupráce mezi lidmi a AI k samostatnému úspěchu AI
V nedávné době se problémy Erdőse staly scénou pro AI průlomy. Prvním krokem bylo „předávání pomyslného štafetového kolíku“ ohledně Erdősova problému č. 367. Matematik Wouter van Doorn navrhl intuici pro důkaz, která však závisela na specifické kongruenční rovnosti. Mistr matematiky a laureát Fieldsovy ceny Terence Tao přebral štafetu a předal tuto rovnici AI modelu Gemini, který byl nedávno populární. Výsledek byl překvapivý: AI dokázala během 10 minut provést komplikované výpočty, které by lidem trvaly dny.
Následně Tao převedl komplexní důkaz AI do podoby čitelné pro lidi. Poslední fázi zahájil matematik Boris Alexeev, který použil AI nástroj „Aristotle“ od společnosti Harmonic a dokázal transformovat důkaz do jazyka Lean za pouhé dvě až tři hodiny, což představovalo formální verifikaci a důkladnou kontrolu na možnosti chybných závěrů AI, přičemž dospěli k závěru, že vyvrátili druhou část problému č. 367 (ale problém nevyřešili zcela).
Tato spolupráce mezi lidmi a AI byla velkým pokrokem v oblasti matematického výzkumu, ale v následujících dnech společnost Harmonic oznámila, že AI „Aristotle“ nově samostatně dokázal problém č. 124, který visel bez odpovědi téměř 30 let. AI nejenže dokázala důkaz, ale také tento proces formálně ověřila v jazyce Lean, což zajistilo naprostou logickou správnost.
Nová éra „intuice a důkazů“: matematikové se nebudou muset obávat o své místo
Vlad Tenev, zakladatel společnosti Harmonic, s nadšením oznámil, že „došlo k éře intuicionálních důkazů“. Věří, že to potvrzuje předpověď Terence Tao, že v budoucnosti budou lidé zodpovědní za navrhování „intuice a hypotéz“, zatímco AI se postará o rigorózní, složité procesy formálního dokazování. Tao také nazval tento přístup intuitivní formalizací.
Tao poznamenal, že i když AI v současnosti řeší relativně jednodušší problémy z dlouhého seznamu obtížných otázek v matematice, ukazuje to, že AI se dostává na práh originálního matematického výzkumu. Tyto nástroje, které neustále zlepšují své schopnosti, poskytnou lidem výzkumníkům možnost smazat snadno řešitelné problémy a vytyčit skutečně obtížné úkoly.
Tento průlom by mohl přinést zásadní paradigmata do matematického světa, kde se dříve matematikové podíleli na každém detailu (psaní důkazů) a v budoucnu se stanou architekty, kteří budou vytvářet plány (poskytovat vysokou úroveň intuice), zatímco AI se postará o praktickou práci (formální verifikaci), což povede k rychlejšímu pokroku v matematickém výzkumu.
