V prosincovém vydání magazínu Scientific American z roku 2025 zdůraznila matematička z Johns Hopkins University, Emily Riehl, že se nebojí ztráty zaměstnání kvůli AI. Riehl v článku uvedla, že i když špičkové modely umělé inteligence (AI) dosahují během předkola Mezinárodní matematické olympiády (IMO) zlatých výsledků, matematika klade důraz na „formální důkaz“, který vydrží logické ověření. Podle Riehlových by velké jazykové modely (LLM) měly sklon chybovat u základních problémů a že počítačoví asistenti pracující s formalizovaným jazykem mají stále dlouhou cestu před sebou, než dosáhnou standardů formální verifikace.
Avšak s neustálým vývojem AI byla její pozice vyvrácena, když se ukázalo, že AI, vybavená formálními důkazními schopnostmi, samostatně vyřešila záhadu, jež se déle než 30 let posouvala.
Paul Erdős a jeho zásadní přínos
Pro pochopení váhy tohoto průlomu je nutné se seznámit s maďarským matematikem Paulem Erdősem, jedním z nejplodnějších matematiků 20. století, který publikoval kolem 1500 článků. Erdős vedl život plný nezávislosti, bez manželství, stabilní práce či domova, putoval po světě s kufrem plným oblečení a zápisníků. S matematickou komunitou komunikoval jako se sociálním zázemím, často se objevoval u kolegů doma, aby oznámil: „Můj mozek je otevřený“, a zapojil se do intenzivního brainstormingového procesu.
Erdős byl známý jako „předkladatel problémů“, neboť celkem navrhl tisíce dosud nevyřešených hypotéz, známých jako „Erdősovy problémy“. Tyto otázky byly odměňovány cenou od 25 do 10 000 dolarů, přičemž jejich vyřešení je považováno za značný úspěch v matematice.
Od spolupráce mezi člověkem a AI k samostatnému vyřešení problémů
V poslední době se platforma Erdősových problémů stala místem, kde došlo k významnému průlomu. V průběhu „štafety mezi člověkem a AI“ se matematik Wouter van Doorn pokusil dokázat určitou hypotézu, která se opírala o specifický kongruenční vzorec. V náběhu se k němu přidal laureát Fieldsovy medaile Terence Tao, který zadal problém do nedávno vydaného AI modelu Gemini od Google. AI dokončilo složité výpočty, které by lidským matematikům trvaly několik dní, během pouhých deseti minut.
Poté Tao přepracoval složitý důkaz AI do lidsky čitelné podoby. Závěrečnou fázi zajistil matematik Boris Alexeev, který použil AI nástroj „Aristotle“ od společnosti Harmonic, a dokázal převést důkaz do jazyka Lean, což trvalo pouhé dvě až tři hodiny. Poté provedl pečlivou kontrolu, aby zajistil, že nedošlo k žádným chybám a využívání AI a potvrdil, že vyvrátil druhou část problému #367, i když to neznamenalo jeho úplné vyřešení.
Průlomové vyřešení: problém #124
O několik dní později, Harmonic se hrdě ohlásila, že model Aristotle „nezávisle“ prokázal Erdősův problém #124, který se táhl téměř 30 let. AI nejenže poskytla důkaz, ale zároveň formalizovala validaci v jazyce Lean, přičemž zajistila sto procentní logickou správnost.
Thomas F. Bloom, výzkumník z Royal Society University, uznal, že AI provedla formální důkaz bez lidského zásahu, což bylo působivé, avšak poukázal na to, že návrh řešení #124 byl relativně jednoduchý a mohl se již objevit v tréninkových datech. Na druhou stranu odborník na AI na Tchaj-wanu, Fox, zdůraznil, že schopnost AI nezávisle identifikovat a formalizovat tento matematický problém je ohromný krok vpřed a způsob, jakým se AI vyvinula od problematiky #367 k samostatnému vyřešení problému #124, je ohromující.
Nová éra „intuitivního důkazu“ a role matematiků
Tennis zakladatel Vlad Tenev prohlásil, že doba „intuitivního důkazu“ přišla. Věřil, že to potvrzuje predikci Terence Tao: v budoucnu budou lidé zodpovědní za poskytování „intuice a hypotéz“, zatímco AI se postará o náročný a precizní proces formálních důkazů. Tao to nazval intuitivním formalizováním.
Terence Tao vyjádřil, že i když AI řeší relativně jednoduché „nízké plody“ z oblasti dlouhého ocasu matematiky, dokazují to, že AI se dostává k okraji originálního matematického výzkumu. Tyto zdokonalující se nástroje pomohou lidským výzkumníkům odstraňovat nejjednodušší problémy a identifikovat opravdu složité otázky.
Tento průlom by mohl představovat zásadní posun v matematice; zatímco v minulosti byli matematici považováni za dělníky, kteří museli vynaložit úsilí na každý prostor, v budoucnu by se mohli stát architekty, kteří budou zodpovědní za vytváření plánů, zatímco AI se postarají o provádění formálních ověření, což umožní rychlejší pokrok v oblasti matematického výzkumu.
