Uz pomoć umjetne inteligencije otkriveno da je Gödel dokazao stotine nepoznatih teorema

Finski logičar Jan von Plato, koji od 2017. godine na Univerzitetu u Helsinkiju vodi projekat tumačenja neobjavljenih bilježnica Kurta Gödela, godinama je napredovao tempom od otprilike jedne stranice sedmično. U septembru je u posao uključio AI model Claude i u roku od nekoliko dana dobio sveobuhvatan pregled cijelog materijala. Rezultat je iznenadio i njega samog: austrijski logičar dokazao je stotine teorema za koje niko nije znao.

„Bio sam zapanjen", kazao je von Plato. Prema njegovim riječima, bilježnice sadrže desetine rezultata koji su u matematici postali poznati tek sedamdesetih i osamdesetih godina, kao i 14 tema iz logike kojima se niko nije bavio. Gödel je, kaže on, bio daleko ispred svog vremena.

Stenografija koju u svijetu čita šest ljudi

Riječ je o 16 bilježnica, takozvanih „radnih knjiga", koje je Gödel ispisao početkom 1940-ih. Materijal obuhvata 1.009 gusto ispisanih stranica o matematici i logici, a veliki dio napisan je njemačkom stenografijom Gabelsberger, koja je bila zastarjela i u vrijeme kada ju je Gödel koristio. Von Plato ju je sam naučio i kaže da je jedan od samo šest ljudi na svijetu koji je mogu čitati.

Projekat je, kako priznaje, pokrenuo iz praktičnih razloga: bio je pred obaveznim odlaskom u penziju i tražio je način da ostane nezamjenjiv na univerzitetu. Od Evropskog istraživačkog vijeća dobio je grant od 2,5 miliona eura (2,1 milion funti) i okupio mali tim.

Ideja s konferencije u Francuskoj

Prekretnica se dogodila u augustu, na konferenciji o umjetnoj inteligenciji i dokazivanju teorema u Francuskoj, gdje su mu informatičari predložili da u tumačenje bilježnica uključi Claude. Po povratku u Helsinki modelu je dao svoje transkripcije radnih knjiga, šest knjiga koje je ranije napisao o Gödelu i drugu stručnu literaturu.

Za nekoliko dana dobio je objašnjenje radnih knjiga na 650 stranica. Von Plato naglašava da se sve moralo provjeriti stranicu po stranicu, ali da je takav posao za ljude praktično neizvodljiv: čovjek čita jednu stranicu u jednom trenutku, zaboravlja detalje i za 50 stranica mu treba oko godinu dana, dok umjetna inteligencija može povezati sve dijelove hiljadu stranica i sagledati Gödijelove zapise kao jednu cjelinu.

Ko je bio Kurt Gödel

Gödel se smatra jednim od najoriginalnijih mislilaca 20. stoljeća. Njegova dva teorema o nepotpunosti, objavljena 1931. godine, pokazala su da u svakom matematičkom sistemu postoje istinite tvrdnje koje se unutar tog sistema ne mogu ni dokazati ni opovrgnuti. Za prethodne generacije logičara, koji su se nadali da su sve istine provjerljive, to je bio udarac, ali je istovremeno otvorilo nove pravce: Alana Turinga je inspirisalo da 1936. napiše rad kojim je započela teorija modernog računarstva.

Nakon ključnih rezultata iz tridesetih Gödel je objavio tek nekoliko radova, ali njegovi neobjavljeni zapisi broje desetine hiljada stranica. Godine 1940. pobjegao je iz nacističke Austrije i nastanio se u Princetonu, gdje se na Institutu za napredne studije zbližio s Albertom Einsteinom. U kasnijim godinama postajao je sve paranoičniji, odbijao je jesti hranu koju nije pripremila njegova supruga i 1978. umro je od gladi.

Cohenova medalja i dokaz koji je nedostajao

Američki matematičar Paul Cohen 1966. godine dobio je Fieldsovu medalju, najviše priznanje u matematici, jer je pokazao nezavisnost dvije poznate tvrdnje, hipoteze kontinuuma i aksioma izbora. Gödel je na to reagovao tvrdnjom da je isti rezultat već dokazao četrdesetih godina. Kada su kolege zatražile da to i pokaže, iz svojih bilješki nije uspio rekonstruirati dokaz.

Upravo to je bio prvi zadatak koji je von Plato postavio Claudeu: provjeriti sadrže li radne knjige dokaz nezavisnosti aksioma izbora, što bi potvrdilo da je Gödel 1966. govorio istinu. Odgovor je glasio: da, gotovo. „Bio je samo jedan korak udaljen", kaže von Plato. Jednu definiciju Gödel je postavio pogrešno, ali ju je dvije godine ranije imao ispravnu, pa von Plato smatra da bi do nje svakako došao da je nastavio raditi još nekoliko mjeseci.

Arhitekturu dokaza opisuje kao izvanrednu, jer sve rezultate teorije skupova svodi na jedinstven obrazac. Gödela vidi kao mislioca koji polazi od vrlo jasnih ideja i potom ih metodično, korak po korak, provodi do cilja, umjesto da se igra formulama nadajući se da će nekamo stići.

Rekonstruirani dokaz von Plato je potom provjerio u programu Coq, koji ispituje valjanost matematičkih dokaza, i dokaz je prošao provjeru. Uvjeren je da bi Gödel, da je tada objavio rad o aksiomu izbora, osvojio Fieldsovu medalju 1940. godine.

Od 663 teorema oko 400 potvrđeno

Claude je iz radnih knjiga izdvojio ukupno 663 teorema, koji su zatim provjereni u Coqu. Oko 400 ih je potvrđeno kao ispravno, oko 200 je bilo potrebno popraviti, a pedesetak ih je bilo pogrešno. Gödel je, uostalom, i sam bio strog prema vlastitom radu: na marginama bilježnica imao je običaj zapisivati „falsch!" („pogrešno!") ili „schlecht!" („loše!").

Posao time nije završen. Dijelovi bilježnica koji se bave fizikom i kosmologijom, kao i više od desetak tema koje do sada niko nije istražio, tek čekaju daljnje proučavanje.