V roce 2024 oslavila Mezinárodní matematická olympiáda historický milník. Zatímco tato soutěž je tradičně soubojem rozumu mezi nejchytřejšími studenty světa, show ukradl neoficiální účastník: AlphaProof od Google DeepMind. Program umělé inteligence přinesl výsledek na úrovni stříbrné medaile, což dokazuje, že stroje již nejsou jen skřípání čísel – začínají ovládat umění logického uvažování.
Tento průlom není izolovaným inženýrským zázrakem; je to výsledek desetiletí dlouhého vývoje toho, jak testujeme pravdu pomocí kódu. Novinář Kevin Hartnett ve své nové knize The Proof in Code zkoumá neuvěřitelnou cestu Leanu, softwarového nástroje, který se vyvinul ze speciálního nástroje pro kódování k základům moderní matematické verifikace a vývoje AI.
Most mezi kódem a logikou
Příběh začíná Leo de Mourou, bývalým inženýrem Microsoft Research, který spustil Lean v roce 2013. Původně byl Lean vyvinut jako nástroj pro kontrolu chyb v kódu programu, ale měl skrytý potenciál díky své strukturální podobnosti s matematikou.
Jak poznamenává Hartnett, tyto dvě disciplíny sdílejí základní DNA:
– Syntaxe: Oba vyžadují přesné pokyny krok za krokem.
– Logic: Jediná chyba v řádku kódu je funkčně identická s “mezerou” v matematickém důkazu.
– Provedení: Stejně jako program běží pouze tehdy, je-li logika správná, matematická věta je považována za pravdivou pouze tehdy, když je její důkaz bezchybný.
Toto poznání dalo impuls novému hnutí. Ačkoli Lean nedokázal samostatně „vynalézt“ novou matematiku, fungoval jako interaktivní dokazovač teorému. Mohl by vzít důkaz napsaný osobou – což by mohlo zabrat stovky stran a měsíce přezkoumání – a okamžitě potvrdit jeho absolutní správnost.
Boj o „matematický jazyk“
Přechod od tradiční matematiky k digitálním důkazům nebyl hladký. Po celá léta matematici čelili klasickému problému „kuře a vejce“: aby byl Lean užitečný, potřebovali obrovské knihovny kódovaných matematických definic; ale k vytvoření těchto knihoven potřebovali matematiky, kteří by program používali.
Tření bylo často absurdně detailní. Hartnett popisuje, jak se profesor Kevin Buzzard z Imperial College v Londýně zadrhl při výuce studentů, protože Lean po něm požadoval, aby dokázal, že 2 se nerovná 1. Pro člověka je to zjevná pravda; pro systém formální logiky je to základní fakt, který musí být explicitně definován předtím, než bude možné provést jakékoli další uvažování.
Překonání těchto překážek vyžadovalo obrovské kolektivní úsilí:
* Digitalizace ve velkém: V roce 2018 strávili matematici měsíce překládáním složitých konceptů, jako jsou „perfektoidní prostory“ do tisíců řádků kódu.
* Budování komunity: Malá skupina oddaných výzkumníků pracovala na tom, aby byl software uživatelsky přívětivý a přeměnili jej z těžkopádného akademického nástroje na robustní platformu.
* Škálování: Do roku 2025 ekosystém explodoval a do Lean knihoven přispívaly desítky tisíc uživatelů z akademické sféry a technického průmyslu.
Proč je to důležité: Hledání „stroje pravdy“
Sloučení matematiky a umělé inteligence je konečným cílem tohoto hnutí. Pro softwarové inženýry, jako je de Moura, byla cena „strojem na pravdu“, který dokázal zajistit, že software jako Microsoft Word bude zcela bez chyb. Pro matematiky je to způsob, jak zajistit, že ani ty nejsložitější a nejabstraktnější objevy nebudou zpochybněny.
Pro výzkumníky AI slouží Lean jako ideální tréninkové hřiště. Tím, že poskytuje obrovskou ověřenou knihovnu matematických pravd, umožňuje Lean modelům jako AlphaProof zvládnout přísné uvažování spíše než jen rozpoznávání vzorů. To je zásadní pro vyřešení problému „halucinací“ AI – tendence modelů spolehlivě uvádět nepravdivé informace. Pokud se umělá inteligence naučí dodržovat přísné a neochvějné zákony matematické logiky, bude nakonec schopna aplikovat stejnou přísnost na uvažování v reálném světě.
„[matematika i programování] jsou psány s přesnou syntaxí jako série logických kroků, z nichž každý vede k dalšímu.”
Závěr
Proof in Code vypráví příběh o tom, jak se specializovaný nástroj pro ladění softwaru stal základem pro novou éru matematické jistoty a inteligence AI. Zdůrazňuje hluboký posun ve vědě: směřování k budoucnosti, kde lidská intuice a digitální ověřování spolupracují na určení toho, co je pravda.
