Veštačka inteligencija pomogla je istraživačima da dešifruju više od hiljadu stranica rukopisa jednog od najznačajnijih matematičkih logičara 20. veka. U njima su pronađeni tragovi stotina teorema i ideja koje su decenijama ostale nepoznate naučnom svetu.
Kurt Gედel (Kurt Gödel), austrijski matematičar i logičar koji je svojim radom promenio način na koji razumemo matematiku, možda je tokom života otkrio mnogo više nego što se do sada verovalo. Njegove beležnice, koje su decenijama predstavljale gotovo nerešivu zagonetku za istraživače, uz pomoć veštačke inteligencije otkrile su stotine do sada nepoznatih matematičkih rezultata.
Projekat koji od 2017. godine vodi finski logičar Jan fon Plato sa Univerziteta u Helsinkiju usmeren je na proučavanje 16 Gedelovih beležnica nastalih početkom četrdesetih godina prošlog veka. Reč je o ukupno 1.009 stranica gustog matematičkog teksta, od kojih je veliki deo napisan Gabelsbergerovom stenografijom, sistemom skraćenog pisanja koji je već u Gedelovo vreme bio zastareo.
Fon Plato je godinama pokušavao da razume sadržaj rukopisa. Napredak je bio izuzetno spor – istraživači su uspevali da obrade svega jednu stranicu nedeljno. Situacija se promenila u septembru 2026. godine, kada je finski logičar odlučio da u istraživanje uključi model veštačke inteligencije Claude.
Rezultati su ga potpuno iznenadili.
Za svega nekoliko dana, Claude je pripremio objašnjenje od približno 650 stranica, povezujući različite delove Gedelovih beležnica u jedinstvenu celinu. Veštačka inteligencija uspela je da identifikuje 663 teoreme za koje je Gedel imao dokaz, skicu dokaza ili barem ideju kako bi do njega mogao da dođe.
Od tog broja, približno 400 matematičkih tvrdnji potvrđeno je u obliku u kojem su navedene. Oko 200 zahtevalo je određene ispravke ili preciznije definicije, dok se za približno 50 ispostavilo da su netačne.
Ipak, značaj otkrića ne leži samo u broju pronađenih teorema. Prema Fon Platu, beležnice sadrže više od desetak istraživačkih pravaca u matematičkoj logici i osnovama matematike koji nisu dalje razvijani u decenijama nakon što ih je Gedel zapisao.
Dokaz koji je mogao da promeni istoriju matematike
Jedan od najzanimljivijih delova istraživanja odnosi se na aksiomu izbora, jednu od važnih tvrdnji teorije skupova.
Američki matematičar Pol Koen (Paul Cohen) dobio je 1966. godine Fildsovu medalju, najprestižnije priznanje u matematici, između ostalog za rezultate koji su pokazali nezavisnost određenih matematičkih tvrdnji od prihvaćenih aksioma teorije skupova.
Gedel je tada tvrdio da je sličan rezultat dokazao još tokom četrdesetih godina. Međutim, nije uspeo da svojim kolegama ponovo pokaže dokaz.
Fon Plato je zato od Claudea zatražio da ispita da li se u beležnicama nalazi dokaz koji bi potvrdio Gedelovu tvrdnju.
Veštačka inteligencija pronašla je strukturu dokaza, ali i jednu važnu grešku u definiciji koju je Gedel koristio. Prema Fon Platu, matematičar je bio veoma blizu ispravnog rešenja, a u ranijim beleškama čak je imao i odgovarajuću definiciju.
Rekonstruisani dokaz zatim je proveren pomoću programa Coq, računarskog sistema namenjenog formalnoj verifikaciji matematičkih dokaza. Provera je prošla, što je dodatno potvrdilo matematičku ispravnost rekonstruisanog postupka.
Ko je bio Kurt Gedel?
Kurt Gedel rođen je 1906. godine u Brnu, tadašnjoj Austrougarskoj, a ostao je upamćen kao jedan od najuticajnijih matematičkih logičara u istoriji.
Njegove dve teoreme o nepotpunosti, objavljene 1931. godine, pokazale su da postoje ograničenja onoga što je moguće dokazati unutar formalnih matematičkih sistema. Pojednostavljeno, u dovoljno snažnim i doslednim matematičkim sistemima postoje tvrdnje koje se ne mogu dokazati niti opovrgnuti korišćenjem pravila samog sistema.
Ovi rezultati promenili su temelje matematičke logike i uticali na razvoj teorije računarstva. Posebno su inspirisali Alana Tjuringa, čiji je rad iz 1936. godine postavio temelje moderne teorije izračunljivosti.
Gedel je 1940. godine, bežeći od nacističkog režima, napustio Austriju i preselio se u Sjedinjene Američke Države. Živeo je u Prinstonu, gde je radio na Institutu za napredne studije i sprijateljio se sa Albertom Ajnštajnom.
Preminuo je 1978. godine, a poslednje godine života obeležili su ozbiljni problemi sa paranojom i odbijanjem hrane koju nije pripremila njegova supruga. Umro je od posledica neuhranjenosti.
Može li veštačka inteligencija da otkrije ono što ljudi nisu uspeli?
Istraživanje Gedelovih beležnica pokazuje koliko veštačka inteligencija može da bude koristan alat u nauci, posebno kada je potrebno povezati ogromne količine informacija koje bi ljudskim istraživačima oduzele godine rada.
Ipak, to ne znači da je AI samostalno rešio matematičke probleme ili da je preuzeo ulogu naučnika. Fon Plato je morao da proverava rezultate, a za formalnu potvrdu matematičkih dokaza korišćen je i specijalizovani softver Coq.
Profesor logike sa Univerziteta Notr Dam, Džoel Dejvid Hemkins, koji nije imao priliku da pregleda rekonstruisani dokaz, ocenio je da bi njegovo potvrđivanje predstavljalo izuzetno zanimljiv istorijski događaj. Ipak, upozorio je da tek treba utvrditi koliko je u tim rezultatima Gedelovog originalnog rada, a koliko doprinosa savremenih AI sistema.
Fon Plato veruje da bi dalja analiza Gedelovih rukopisa mogla da donese još iznenađenja. Posebno ga zanimaju beležnice koje se odnose na fiziku i kosmologiju, čiji sadržaj tek treba detaljnije istražiti.
Više od osam decenija nakon što ih je zapisao, Gedelovi matematički zapisi tako bi mogli da postanu izvor novih naučnih otkrića.
