Matematičar Kevin Bazard sa Imperijal koledža u Londonu obučava računare da dokažu jedan od najpoznatijih problema u istoriji matematike: Fermaovu poslednju teoremu.
Rešavanje tog problema nije poenta. Već postoji prihvaćen dokaz koji je finalizovan 1998. godine. Taj rad je složeni lavirint matematike koji obuhvata oko 130 stranica u dva rada. On obuhvata više matematičkih oblasti i ujedinjuje apstraktne ideje koje su ranije izgledale nepovezano.
Poznavati taj dokaz znači poznavati širok deo matematike. U budućnosti, kaže Bazard, računarski program koji može da verifikuje nešto tako obimno moći će da pomogne matematičarima da pronađu, analiziraju i rešavaju širok spektar problema.
Bazard i nekolicina matematičara godinama unazad rade na projektima poput ovog
Godinama Bazard i nekolicina matematičara rade na projektima poput ovog kako bi formalizovali matematiku. Istorijski gledano, formalizacija je podrazumevala izražavanje matematičkih ideja što preciznije, uz uklanjanje svake dvosmislenosti. Danas to znači prevođenje definicija i teorema u računarski kod kako bi specijalizovani program mogao da proveri svaki detaljan korak.
Formalizacija „je nova paradigma… koja suštinski zahteva da onaj ko piše dokaz bude mnogo rigorozniji nego inače“, kaže matematičarka Emili Riel sa Univerziteta Džons Hopkins. „Računar zapravo ne popunjava detalje.“ Osoba koja piše dokaz mora da ih uradi sama.
Ali formalizovanje dokaza Fermaove poslednje teoreme je samo temelj šire vizije: izgradnje digitalne biblioteke cele matematike koja će omogućiti računarima da postanu korisni asistenti matematičarima.
Matematika između table i računara
Čak i danas, većina matematičara piše dokaze koristeći opise i intuiciju, tradicionalne alate koji su do nedavno izgledali nedostupni računarima. Zbog toga je formalizacija dugo bila nišna aktivnost jer zahteva izražavanje matematičkih ideja kao koda.
Sada, eksplozija veštačke inteligencije ubrzala je napore, predvođene tehnološkim kompanijama, da se kombinuju veliki jezički modeli sa dokazivačima teorema radi razvoja sistema sposobnih za automatsku formalizaciju. U teoriji, takvi sistemi bi mogli da urade stvari koje ljudi ne mogu.
To je podeljen cilj, koji zabrinjava mnoge matematičare zbog toga kako bi mogao da promeni istraživanje i napredak u matematici. Ono što je počelo kao filozofsko pitanje — koja je maksimalna preciznost matematičkog dokaza — sada je postalo egzistencijalno: da li će težnja ka preciznosti uzdrmati celu oblast?
„Nalazimo se na pragu promene“, kaže Patrik Šafto, matematičar i informatičar sa Rutgersa i DARPA.
„Matematika se danas praktikuje na tabli, kao pre 100 godina. Ali mislim da je vrlo verovatno da će za pet godina svaki mladi matematičar koristiti AI.“
Moj robotski asistent
Ideja korišćenja mašina za dokaze nije nova. Već 1956. godine istraživači RAND korporacije predstavili su računarski program (nazvali su ga „logička teorijska mašina“) koji je proveravao dokaze iz Principia Mathematica, čuvenog dela Bertranda Rasela i Alfreda Norta Vajtheda.
„Oduševljen sam što Principia Mathematica sada može da se radi mašinski“, napisao je Rasel u pismu Herbertu Sajmonu, jednom od tvoraca sistema. „Žao mi je što Vajthed i ja nismo znali za tu mogućnost, jer smo izgubili 10 godina radeći ručno.“
Iako nije postala široka praksa, neki matematičari su poslednjih decenija koristili interaktivne dokazivače teorema za proveru postojećih dokaza. Jedan od najpoznatijih primera je 1998. godine, kada je matematičar Tomas Hejls objavio da je sa svojim studentom Samjuelom Fergusonom koristio računar da dokaže Keplerovu hipotezu, problem optimalnog pakovanja sfera koji je postavio Johanes Kepler u 17. veku.
Otpor i formalizacija Keplerove hipoteze
Dokaz je naišao na otpor među matematičarima, koji su tvrdili da zbog ogromnih i složenih računskih provera ljudi ne mogu ručno da potvrde svaki korak, pa samim tim ni da u potpunosti verifikuju ispravnost dokaza.
Zbog toga je od 2003. do 2014. godine Hejls koristio digitalne asistente kako bi formalizovao i ponovo proverio sopstveni dokaz.
U februaru, kombinovanjem veštačke inteligencije i interaktivnog dokazivača teorema, ukrajinska matematičarka Marina Viazovska i drugi završili su formalizaciju dokaza Keplerove hipoteze u osam i 24 dimenzije — digitalne verzije rada koji je Viazovskoj doneo Fildsovu medalju 2022. godine.
Bazardov put ka formalizaciji
Bazardov rad sa formalizacijom počeo je 2017. godine, kada je, kako kaže, prošao kroz neku vrstu „matematičke krize“. Upravo je bio recenzent jednog rada za naučni časopis i nakon duge prepiske sa autorom nije mogao da utvrdi da li je argument zaista rigorozan.
Ta frustracija ga je navela da preispita stanje u matematici i ono što bi ona mogla da postane. „Bio sam prilično nezadovoljan stanjem stvari“, rekao je tokom jednog predavanja. Počeo je da se pita: da li tehnologija može da ukloni neizvesnost u verifikaciji dokaza?
Matematičari ne ulaze u ovu oblast zato da bi proveravali detalje tuđih dokaza, već da bi otkrivali nove stvari. Ako bi verifikacija mogla da se prepusti mašini, zašto to ne iskoristiti?
Lean i digitalizacija matematike
Bazard je počeo da uči Lean, koji je i programski jezik i interaktivni dokazivač teorema. Lean se pojavio 2013. godine, a razvio ga je Léo de Mora, kompjuterski naučnik iz Microsoft-a, kao sistem za formalnu verifikaciju matematičkih argumenata.
Lean je isti sistem koji je korišćen za formalizaciju Viazovskovih dokaza u februaru.
Kako je Bazard sve više učio, postajao je sve uzbuđeniji. Počeo je da formalizaciju vidi kao digitalizaciju matematike, što bi moglo da modernizuje način na koji matematičari koriste računare.
On to upoređuje sa digitalizacijom muzike. Kada su muzičke kompanije počele da prodaju CD-ove, isprva je to delovalo kao način da se ljudi nateraju da ponovo kupuju ono što već imaju. Ali kasnije je omogućilo nove načine pristupa i deljenja muzike, što je dodatno ubrzano strimingom.
„Digitalizacija muzike je potpuno promenila svet muzike“, kaže Bazard. „Ako digitalizujemo matematiku, možda će i ona biti potpuno promenjena.“
Velika misterija u maloj margini
Prema legendi, oko 1637. godine francuski matematičar Pjer de Ferma je zapisao problem i napomenu u primerak knjige Arithmetica, dela grčkog matematičara Diofanta iz trećeg veka. Problem se odnosi na jednačinu:
an + bn = cn
Ako je n = 2, znamo da postoji beskonačno rešenja. U tom slučaju jednačina postaje Pitagorina teorema, gde a, b i c predstavljaju stranice pravouglih trouglova.
Ferma je tvrdio da ne postoje celi brojevi a, b i c koji mogu da zadovolje ovu jednačinu ako je n veće od 2. Pored problema je napisao na latinskom: „Imam zaista čudesan dokaz ove tvrdnje, ali je ova margina suviše uska da ga sadrži.“
Vekovi bez dokaza
Fermin sin je kasnije pronašao knjigu i belešku, ali tek posle očeve smrti. Teorema je bila jednostavna za formulisanje, ali izuzetno teška za dokazivanje, i Fermin „izgubljeni dokaz“ je vekovima zbunjivao matematičare.
Nije nikada pronađen njegov dokaz, a mnogi sumnjaju da je uopšte postojao ili da je bio netačan. Neki čak misle da je cela tvrdnja bila neka vrsta intelektualne šale koja je trajala vekovima.
Endru Vajls i rešenje problema
Britanski matematičar Endru Vajls konačno je rešio problem krajem 20. veka, a kasnije je sarađivao sa Ričardom Tejlorom kako bi dokaz finalizovali.
Njihov dokaz je koristio duboke i veoma apstraktne matematičke koncepte koji nisu postojali u 17. veku, povezujući oblasti matematike koje su se ranije smatrale nepovezanim.
Posledice Fermaovog problema
Kroz vekove, proučavanje ovog jednostavnog problema dovelo je do velikih otkrića u matematici, posebno u teoriji brojeva.
Jedan od najvažnijih doprinosa došao je 1847. godine kada je nemački matematičar Ernst Kumer dokazao da teorema važi za određene proste brojeve. On je razvio ideje koje su postale temelj nove oblasti — algebarske teorije brojeva.
Bazard i formalizacija Fermaove teoreme
Godine 2023. Bazard je pokrenuo projekat formalizacije Fermaove poslednje teoreme, delimično zbog njene važnosti i veličine, a delimično zato što mnoge njegove kolege sa Imperijal koledža istražuju ideje koje se pojavljuju u dokazu.
On je znao da će to biti ogroman i složen posao, jer je potrebno formalizovati svaku definiciju i svaku pomoćnu teoremu koja se koristi u dokazu. Projekat je, kaže, bio težak i pun neuspelih pokušaja.
Veliki i rastući projekat
Bazard ne radi sam. U početku, kaže on, oko 30 ljudi je učestvovalo u projektu formalizacije, svi su pisali kod za Lean i bili su poznati saradnici. Mnogi drugi su se javljali sa idejama ili pokušavali da se uključe, a nešto više od 60 ljudi je imalo svoje doprinose koji su verifikovani i prihvaćeni.
Ipak, projekat je prerastao u interdisciplinarnu saradnju na nivou koji Bazard nije očekivao. Anonimni teoretičari brojeva šalju ideje, kaže on. Prošlog avgusta, bio je na muzičkom festivalu nedelju dana i vratio se sa 7.000 nepročitanih poruka u vezi različitih delova dokaza.
U januaru je projekat dostigao jednu od prvih važnih prekretnica. „Dokazali smo da je određena stvar konačna“, kaže Bazard, što je omogućilo sledeći korak. Međutim, napor koji je bio potreban za tu prekretnicu naveo ga je da sumnja da će uspeti da završe u planiranom roku od pet godina.
Problem baze znanja u matematici
Jedan od najvećih izazova je izgradnja biblioteke matematičkog znanja unutar Lean sistema. Bazard kaže da je to usko grlo i za primenu veštačke inteligencije u matematici.
„U ovoj oblasti AI za matematiku postoji veliki problem — nedostaju nam kvalitetni i zanimljivi skupovi podataka“, kaže on.
U drugom projektu, koji finansira Renaissance Philanthropy, Bazard i matematičar sa Rutgersa Aleks Kontorovič dodatno razvijaju Lean biblioteku i proširuju njenu primenu formalizacijom savremenih teorema koje predstavljaju vrhunska dostignuća matematike 21. veka.
Posledice šire od jednog projekta
Proširenje matematičkog znanja u digitalnom obliku moglo bi omogućiti matematičarima da otkriju greške u novim dokazima ili da procene da li određene hipoteze uopšte mogu da stoje.
Recenzenti naučnih časopisa mogli bi da se više fokusiraju na ideje, umesto na proveru tehničkih detalja dokaza.
„To menja pravila igre“, kaže Riel. „Dokazi su dugi i složeni, i greške se lako provuku.“
AI kao alat za proveru dokaza
Dokazivač teorema koji ima pristup velikoj matematičkoj bazi mogao bi da prepozna greške, halucinacije i netačnosti u dokazima koje generiše AI.
Bazard kaže: „Jedna halucinacija može da uništi ceo matematički argument, jer je matematika takva.“
Zbog toga tehnološke kompanije razvijaju sisteme koji kombinuju modele kao što su Google Gemini i ChatGPT sa Lean dokazivačem.
Rastući AI izazov
Do sada je glavni problem velikih jezičkih modela u matematici bio tačnost. Modeli poput ChatGPT-a i Claude-a su bolji u matematici nego što se očekivalo, i stalno napreduju, ali i dalje prave greške.
„Ako odete na ChatGPT i tražite da dokaže teoremu, on će vam ispisati tekst“, kaže Riel. „Može zvučati dobro i koristiti ispravne termine, ali nema garancije da je ispravno.“
Kada se kombinuju sa dokazivačima teorema poput Lean-a, modeli postaju mnogo pouzdaniji.
AI na nivou matematičkih olimpijada
Prošlog jula, kompanija Harmonic predstavila je sistem Aristotle, koji koristi Lean za proveru i doradu rešenja. On je postigao rezultat na nivou zlatne medalje na Međunarodnoj matematičkoj olimpijadi.
Na takmičenju u Australiji 2025. godine, više od 600 učesnika je rešavalo izuzetno teške zadatke, a samo 72 je osvojilo zlato.
Slične rezultate postigli su i sistemi Google-a i OpenAI-a.
AI, formalizacija i novi rezultati
Kasnije su istraživači sa Rutgersa i UCLA radili na formalizaciji „teoreme o prostim brojevima“. Napredak je bio spor, ali je kompanija Math, Inc., uz podršku DARPA programa, uspela da završi posao za samo tri nedelje koristeći sistem Gauss.
Taj sistem kombinuje Lean i AI modele koji automatski prevode dokaze u formalni oblik koji Lean proverava.
Slično tome, istraživači su koristili sisteme kao što su Aristotle i GPT-5.2 da generišu i formalizuju dokaze problema koje je postavio Pol Erdoš.
Sumnje i ograničenja
Ipak, Bazard je i dalje skeptičan. Kaže da trenutno ne postoje prave „zaštite“ u sistemima.
Iako Lean može da potvrdi formalnu ispravnost koda, to ne znači da AI nije pogrešno protumačio šta se uopšte dokazuje.
„Može se desiti da sve izgleda ispravno, ali da zapravo nije dokazano ono što smo mislili“, kaže on.
Budućnost matematike
Neki matematičari veruju da će ljudi uvek biti neophodni, ali da će njihova uloga biti drugačija.
„Deo rešavanja problema će praktično nestati“, kaže Kristijan Segedi. Uloga ljudi će biti da usmeravaju matematiku ka zanimljivim pravcima, dok će AI obavljati tehnički deo.
On predviđa da će AI uskoro postati superioran u formalizaciji dokaza i da će jednog dana moći da stvara dokaze od početka do kraja.
Strahovi i kritike
Drugi matematičari su zabrinuti. Arvind Asok smatra da AI pojednostavljuje matematiku na pogrešan način i da ne razume njenu suštinu.
On je čak prestao da daje domaće zadatke jer studenti previše koriste AI.
Postoji strah da će nove generacije izgubiti sposobnost dubokog razmišljanja ako se previše oslone na mašine.
Bazard, međutim, tvrdi da cilj nije zamena matematičara, već pomoć.
„Samo želim da učinim život svojih kolega lakšim. Ne da ih zamenim. Zapravo pokušavam da pomognem.“
