Umělá inteligence nezávisle ověřila důkaz jednoho z nejobtížnějších problémů v matematice – problém nejhustšího shlukování koulí v multidimenzionálním prostoru – což je výkon, který v roce 2022 vynesl ukrajinské matematičce Marině Vjazovské Fields Medal. Tento milník znamená zásadní posun ve způsobu, jakým je matematický výzkum prováděn, a přechází od umělé inteligence jako nástroje pouhého kolaborativního uvažování.
Vyvíjející se role umělé inteligence v matematice
Po staletí se matematici při výpočtech spoléhali na nástroje jako abaci, kalkulačky a počítače. Tyto nástroje však zůstaly rozšířením lidské inteligence a nikdy nenahradily základní proces uvažování. Moderní nástup umělé inteligence v matematice je zásadně odlišný: tyto systémy nyní pomáhají nejen s výpočty, ale i se samotným uvažováním, čímž automatizují mnoho kroků, které jsou základem matematických argumentů.
K tomuto posunu docházelo postupně. Moderní matematika již spoléhá na složité struktury a rozsáhlé katalogy výsledků, kterým nikdo nemůže plně porozumět. Počítače již pomohly při velkých důkazech, jako je čtyřbarevný teorém a Keplerova domněnka, ale dnešní systémy umělé inteligence nabízejí novou úroveň autonomie a spolehlivosti, zejména v kombinaci s asistenty formálního důkazu.
Síla formálního ověření
Formální ověřovací jazyky, jako je Lean, vyjadřují matematické argumenty způsobem, který umožňuje počítačům ověřit každý krok a zajistit logickou platnost. Na rozdíl od tradičního matematického psaní vyžaduje Lean explicitní definice a závěry a pečlivě testuje každý krok. I když je to nelítostné, tento proces eliminuje skryté domněnky a skoky víry. Výsledek je určen matematicky za předpokladu, že důkaz projde testem Lean.
Během několika posledních let matematici vybudovali rozsáhlé knihovny v těchto jazycích, shromáždili definice a osvědčené teorémy k řešení stále složitějších problémů. Dříve byl úzkým místem pracný proces převádění nejmodernějších důkazů do strojově ověřitelné podoby, což byl úkol, který mohl trvat měsíce nebo roky.
Průlom: Vyazovskaya Proof, AI ověřeno
Nedávné ověření důkazu nejhustšího balícího problému pro sféry v multidimenzionálním prostoru Vjazovskaja ukazuje rychlý pokrok v této oblasti. Problém nejhustšího uspořádání koulí se ptá, jak hustě identické koule mohou být zabaleny v prostorech jakékoli dimenze. Vjazovskaja tento problém vyřešila pro osm a 24 dimenzí, přičemž navázala na práci, která byla dříve dokončena pouze pro jeden, dva a tři rozměry.
Startup AI Math, Inc., používající svého Gaussova logického agenta, sehrál klíčovou roli při překladu argumentů Vjazovské do Lean kódu a ověřování každého kroku. Systém AI nefungoval izolovaně: matematici poskytli počáteční plán a strukturu. Po nastavení však Gauss dokončil práci během několika dní – úkol, který podle lidských výzkumníků zabere měsíce.
Budoucnost matematického výzkumu
To je více než jen technický úspěch; to signalizuje zásadní posun ve způsobu práce matematiků. Fields Medalist Terence Tao naznačuje, že okamžitá hodnota umělé inteligence spočívá v automatizaci zdlouhavých, ale koncepčně jednoduchých úkolů, což matematikům umožňuje soustředit se spíše na strategii než na účetnictví. Toto oddělení generování kreativních nápadů od přísného testování je klíčové.
Kevin Buzzard z Imperial College London varuje před spoléháním se na nevyzkoušené velké jazykové modely, ale tvrdí, že formální ověřovací jazyky, jako je Lean, nabízejí řešení. Pokud důkaz projde programem, je zaručeno, že je platný. Hlavní výzvou je nyní převést většinu moderní matematiky do těchto formálních knihoven a poskytnout systémům umělé inteligence potřebné koncepty pro práci.
Závěr
AI nenahrazuje matematiky, ale nově definuje jejich roli. Budoucnost matematiky bude pravděpodobně zahrnovat vytváření a ladění nástrojů, které posouvají lidské kognitivní limity, a spojují intuici se strojovou disciplínou. S rozšiřováním testovatelné matematiky bude větší poptávka po lidech, kteří umí klást správné otázky, vytvářet nové definice a rozpoznávat skutečné myšlenky. Partnerství mezi lidskou inteligencí a umělou inteligencí podnítí novou éru matematických objevů.
