Formální důkaz bez formálního vzdělání: AI sklízí úspěch ve světě čísel
Shutterstock.com
AI dobývá matematiku: Umělá inteligence na stopě Erdősovým problémům
Neel Somani si o víkendu chtěl jen ověřit, jak si ChatGPT poradí s otevřenými matematickými problémy. Vložil jeden z nich do rozhraní a nechal model 15 minut „přemýšlet“. Když se vrátil, čekalo ho překvapení: ChatGPT předložil kompletní důkaz. Somani výsledek formálně ověřil pomocí nástroje Harmonic – a vše sedělo.
šéfredaktor
„Chtěl jsem zjistit, kde mají jazykové modely ještě mezery a kde už naopak zvládají samostatně pracovat,“ říká Somani. A s příchodem nejnovější verze GPT 5.2 se hranice skutečně posunula.
Erdősova výzva a AI v první linii
Problém, který Somani zadal, pochází z rozsáhlé sbírky více než tisícovky matematických domněnek Paula Erdőse, která je veřejně dostupná online. Právě tyto úlohy dnes fungují jako zkušební kámen pro AI – jejich obtížnost i zaměření jsou různorodé, což z nich činí ideální testovací pole.
Od loňského listopadu, kdy se poprvé prosadil model AlphaEvolve od Gemini, se AI začala výrazněji prosazovat. S novou verzí ChatGPT 5.2 to však nabralo na obrátkách. Od Vánoc bylo na webu označeno 15 problémů jako vyřešené a 11 z nich přímo přiznává zapojení AI.
ChatGPT při tom neimprovizuje. Pracuje s axiomaty jako Legendreho formule, Bertrandova hypotéza nebo Star of David teorém. V jednom případě dokonce nalezl a využil řešení z diskuze na Math Overflow z roku 2013 od Noama Elkiese, profesora z Harvardu. Přesto ale předložil jiný, ucelenější důkaz k variantě problému, jak ho kdysi formuloval sám Erdős.
Formalizace mění pravidla hry
Zásadní roli hraje i trend formalizace – převodu důkazů do přísně logické, strojově ověřitelné formy. Ten sám o sobě AI nevyžaduje, ale nové nástroje jako Lean či Aristotle od Harmonicu tuto práci významně usnadňují.
Podle Tudora Achima, zakladatele Harmonicu, není klíčové to, že AI pomáhá řešit slavné problémy, ale to, kdo se k jejímu použití hlásí. „Více mě zajímá, že s těmito nástroji pracují uznávaní profesoři. Když někdo z nich řekne, že používá Aristotela nebo ChatGPT, je to důkaz sám o sobě,“ říká Achim.
Dlouhý ocas problémů pro AI
Do debaty přispěl také respektovaný matematik Terence Tao. Na síti Mastodon napsal, že systematická povaha AI ji předurčuje k řešení „dlouhého ocasu“ méně známých Erdősových problémů – tedy těch, které dosud ležely ladem. „Mnohé z těchto jednodušších úloh teď pravděpodobněji vyřeší čistě AI než člověk,“ konstatuje Tao.
Na svém GitHubu zaznamenává osm případů, kde AI udělala samostatný pokrok, a dalších šest, kde pomohla rozvinout předchozí výzkum. Umělá inteligence sice ještě matematiku zcela neovládla, ale zjevně má své místo. Možná ne jako náhrada, ale jako cenný spoluhráč.
