V prosincovém vydání časopisu Scientific American z roku 2025 se americká matematička z Johns Hopkins University, Emily Riehl, vyjádřila k obavám, že by umělá inteligence (AI) mohla nahradit lidské matematiky. I přes úspěchy AI modelů na mezinárodních matematických soutěžích, jako je Mezinárodní matematická olympiáda (IMO), zdůraznila, že matematika se stále soustředí na formalizované důkazy. Podle ní velké jazykové modely (LLM) dělají chyby v základních úlohách a počítačové asistenty, které pracují s formalizovaným jazykem, čeká ještě dlouhá cesta, aby dosáhli standardů formální verifikace. Avšak s rychlým pokrokem ve vývoji AI je její názor již brzy vyvstán, když AI nedávno samostatně vyřešila matematický problém, který byl visící po desetiletí.

Pochopení významu průlomu: Paul Erdős

Abychom porozuměli tomuto zásadnímu pokroku, je důležité se seznámit s maďarským matematikem Paulem Erdősem. Je jedním z nejplodnějších matematiků 20. století a během svého života publikoval přibližně 1500 vědeckých prací, což nikdo nepřekonal. Erdős vedl volný život bez manželství, stálé práce nebo bydlení, cestoval po světě s kufrem naplněným oblečením a zápisníkem. Vnímal matematiku jako sociální aktivitu a objevoval se u dveří svých kolegů s výrokem: „Můj mozek je otevřený“, aby navázal diskuzi o matematických problémech.

Erdős byl uznáván za „navrhovatele problémů“, když během svého života předložil více než tisíc nevyřešených konjektur, známých jako „Erdősovy problémy“. Na tyto problémy vypsal odměny od 25 dolarů až po 10 000 dolarů za ty nejkomplexnější, což ukazuje na význam jejich vyřešení v matematické komunitě.

Od spolupráce mezi lidmi a stroji k výlučné úloze AI

V poslední době byla „Erdősova problémová síť“ scénou pro toto AI překročení. Prvním problémem byla Erdősova konjektura č. 367, na kterou matematik Wouter van Doorn předložil protiargument, avšak tento důkaz závisel na specifickém kongruenčním vzorci. Poté se zapojil Terence Tao, nositel Fieldsovy ceny, který předal vzorec AI modelu Gemini od Googlu. Ten dokončil složité ověřování, které by od lidí trvalo několik dní, za pouhých 10 minut.

Následně Tao přetvořil složitý důkaz AI do podoby, kterou mohli lidé číst. Poslední část úkolu obstaral matematik Boris Alexeev, který pomocí AI nástroje firmy Harmonic, známého jako „Aristotle“, převedl důkaz do jazyka Lean za dvě až tři hodiny, úspěšně dosáhl formalizace a důkladně ověřil, zda nejsou přítomny žádné omyly nebo zneužití AI, a potvrdil, že vyvrátil druhou část problému č. 367 (aniž by tento problém zcela vyřešil).

Nová éra „intuice“ v matematických důkazech

Tato lidsko-strojová spolupráce představuje velký pokrok v oblasti matematického výzkumu. Jen pár dní po této události však společnost Harmonic s velkou slávou oznámila, že „Aristotle“ samostatně dokázal vyřešit Erdősův problém č. 124, který zůstal bez odpovědi téměř 30 let. AI nejenže vyřešila důkaz, ale také jej přetvořila do jazyka Lean a zabezpečila tím stoprocentní logickou správnost.

Odborník na matematiku Thomas F. Bloom z Royal Society University ocenil, že AI byla schopna dokončit formalizaci bez lidského zásahu, avšak poukázal na to, že navrhované řešení problému č. 124 bylo relativně snadné a krátké; možno, že se již objevilo v tréninkových datech. Naopak taiwanský expert na AI, Fox Hsiao, zdůraznil, že schopnost AI autonomně lokalizovat a formalizovat tento matematický problém je významným skokem a že její pokrok od asistence při problému č. 367 k autonomnímu řešení č. 124 je ohromující.

Matematici jako dirigenti v nové éře

Vlad Tenev, zakladatel společnosti Harmonic, prohlásil, že doba „intuice v důkazech“ už přišla. Věřil, že to potvrzuje predikci Terence Taa: v budoucnu budou lidé odpovědní za poskytování „intuice a konjectur“, zatímco AI se postará o zvládnutí formalizovaných a pečlivých důkazních procesů, což Tao nazval „intuice formalizací“.

Ve svém příspěvku Tao poznamenal, že i když tyto AI technologie se zaměřují na relativně snazší problémy v delším seznamu matematiky (long tail), představuje to, že AI je na prahu originálního matematického výzkumu, kde tyto stále silnější nástroje pomohou lidským vědcům vyčistit nejzákladnější úkoly a zaměřit se na skutečně složité otázky.

Tento průlom by mohl představovat zásadní posun v oblasti matematiky, kdy předtím byli matematici chápáni jako stavební dělníci, kteří museli osobně přesouvat každý kámen (spisování důkazů). V budoucnu se očekává, že matematici se stanou architekty, kteří budou zodpovědní za plánování (poskytování komplexních intuicí), zatímco AI převezme zodpovědnost za stavbu (formální ověřování), což povede k rychlejšímu pokroku v matematickém výzkumu.