Kraj matematike. Ili (novi) početak

• Naslovna fotografija: Daniel Litt (Izvor: VAST)

Daniel Litt, profesor na Sveučilištu u Torontu, objavio je 14. rujna 2026. esej The End of Mathematics (Kraj matematike), koji je ubrzo prenaslovio u A beginning for mathematics (Početak matematike). Esej je izazvao iznimno burnu raspravu u matematičkoj zajednici. Njegova je premisa da će uskoro postati stvarnost AI sustavi koji su sposobniji od ljudi u većini aspekata matematike te da se zato matematička profesija mora radikalno preobraziti. Promjena naslova je, dakle, opravdana, jer Litt ne predviđa kraj matematike, nego tvrdi da smo na početku njene nevjerojatne eksplozije. Ipak upozorava da bi, bez prilagodbe ključnih institucija, moglo doći do zastoja u našem (ljudskom) razumijevanju matematike. Litt s pravom tvrdi da u matematičkoj zajednici ne postoji konsenzus o tome koji su njeni ciljevi. Jedni misle da je to rješavanje matematičkih problema, drugi da je matematika igra ili poezija, treći žele proniknuti u platonsko carstvo, a neki prenijeti ljubav prema matematici na sljedeću generaciju. On pak drži da su neupitni sljedeći ciljevi:

1. Proizvoditi i razumjeti visokokvalitetnu matematiku.
2. Proizvoditi visokokvalitetne matematičare.

Litt upozorava da te ciljeve već duže vrijeme pokušavamo ostvariti prvenstveno kroz dokazivanje matematičkih teorema, što je nedostatno. Sve je vjerojatnije da je taj cilj jednostavno automatizirati: računalo može početi od neke aksiomatizacije teorije skupova u kojoj se za razmatrani teorem može formalizirati odgovarajuća matematika te iterativno primjenjivati pravila dedukcije. Matematičar je nepotreban. Zato predlaže sljedeći pristup doktoratima iz matematike, koji su ulaznica u ceh matematičara.

• Cilj doktorata je postati svjetski stručnjak za neku zanimljivu, duboku temu i moći prenijeti to razumijevanje drugima.
• Doktorat treba dodjeljivati prvenstveno na temelju rigorozne obrane u kojoj student objašnjava temu ispitivačima sve dok oni ne budu zadovoljni.
• Podrijetlo teme, umjetna inteligencija ili ne, irelevantno je.

Litt također predlaže sljedeće.

• I za posao i za doktorski studij nužni su intervjui, jer razgovor i matematička rasprava danas bolje pokazuju razumijevanje od objavljenih radova.
• Važna je kultura seminara u kojoj se očekuje da predavač objasni temu na zadovoljstvo kompetentne publike.
• Treba nagraditi one istraživačke programe koji uvjere druge u svoju vrijednost, jer je odlučivanje o tome što je zanimljivo postala rijetka vještina.

Litt osim toga tvrdi da se ljude ne može zaustaviti da pritiskom na AI-gumb dokazuju matematičke teoreme i naglašava da podrijetlo dokaza nije važno —važno je njegovo razumijevanje. Ako se matematički problem može AI-gumbom riješiti za cijenu dobre večere, trebamo biti oduševljeni, a ne užasnuti. “Matematika je nekada bila najjeftinija znanost. Mislim da je najveća promjena s kojom se suočavamo to što će se sada na neka naša pitanja moći odgovoriti putem novčane injekcije.” Rasprava koja je uslijedila bila je (i još je uvijek) iznimno je bogata i polarizirana. Evo nekih mišljenja.

“Na neki način, Litt je to razumno napisao, ali čini mi se da više ne želim raditi matematiku.”

“Radije bih napustio matematiku nego pristao na ovu posve distopijsku viziju.“

“Osjećaj da sam uzalud potrošio cijeli svoj odrasli život, prilično je sramotan.”

“Problem Littove optimistične vizije budućnosti je što pretpostavlja da će mladi ljudi htjeti ući u profesiju u njenom novom obliku. Nisam siguran da hoće.”

“Sve se čini tako beznadno. Jedino pitanje koje ostaje je što će prvo ubiti matematiku: potpuni nestanak mladih ljudi koji žele postati matematičari, ili javnost koje će odlučiti da više nema potrebe financirati profesionalne matematičare.”

“Zvuči pomalo kao da matematičari postaju slični pjesnicima i kritičarima poezije. To je u redu, ali tko bi to financirao?”

“Sve rasprave o obuci i ocjenjivanju matematičara su bespredmetne ako javnost odluči ne financirati matematiku.”

“Možete jednostavno zamoliti vodeće AI kompanije da odbiju rješavati matematičke probleme. To već rade za kibernetičku sigurnost, biološko oružje…”

“Nijedna vlada neće zabraniti chatbotovima da rade matematiku… Ovo je vrlo slično strojnom šahistu Deep Blue koji je 1997. koštao 2.5 milijuna dolara, a 30 godina kasnije Stockfish ga na vašem iPhoneu lako pobjeđuje.”

“Ovo je prvi esej iz same profesije koji uzima robusno nadljudski AI kao premisu i zatim pita što bi matematika trebala postati, a ne što u njoj treba braniti.”

“Jedan moj prijatelj voli reći da je glavni razlog zašto društvo treba financirati matematiku, dati pametnim ljudima nešto da rade i spriječiti ih da upadnu u nevolje.”

Daniel Litt odgovara: “Kao što sam napisao, mislim da će modeli biti bolji od nas u rješavanju matematičkih problema i to uskoro. Ono što mislim da bismo trebali učiniti je da se time počnemo baviti, da to pokušamo razumjeti.” Ta je teza nevjerojatno osnažena 6. listopada kada je OpenAI matematički svijet preplavio stotinama AI-generiranih dokaza koji su riješili mnoge dotad neriješene matematičke probleme. Neki su impresivni, a neki čak i spektakularni. Rasprava se može sažeti u dvije suprotstavljene vizije:

Optimistična vizija	Pesimistična vizija
AI će omogućiti matematičarima da se posvete dubljem razumijevanju matematike.	AI će matematičare učiniti suvišnima.
Dolazi zlatno doba matematike.	Dolazi kraj matematičke profesije.
Treba se prilagoditi i redefinirati institucije.	Institucije se ne mogu prilagoditi dovoljno brzo.
Mladi će htjeti biti dio nove matematike.	Mladi neće ulaziti u profesiju.
Javnost će podržati novu matematiku.	Javnost će odustati od financiranja.

Litt zaključuje esej riječima:

“Ima još toliko toga za naučiti — beskonačno mnogo. Uvijek smo bili na početku, i uvijek ćemo biti.”

Esej Daniela Litta će se dugo citirati; ne zato što nudi odgovore, već zato što postavlja prava pitanja u trenutku kada matematička zajednica još nije sigurna kako reagirati na promjenu. Litt ne piše apokaliptični traktat o “kraju matematike”. Naprotiv, tvrdi da smo na početku “nevjerojatne, divne eksplozije matematike”. No, unatoč plemenitoj namjeri, esej pati od niza konceptualnih i empirijskih slabosti koje ga čine manje uvjerljivim nego što bi mogao biti. Litt započinje esej tvrdnjom:

“Ovaj se esej temelji na pretpostavci da će uskoro postojati sustavi umjetne inteligencije koji u većini ili svim aspektima matematike znatno nadmašuju ljudske sposobnosti.”

Premisa je iznimno jaka, ali Litt je ne argumentira – jednostavno je postulira. To je metodološki problem: ako gradite viziju budućnosti profesije na pretpostavci koja nije utemeljena, i zaključci su jednako neutemeljeni. Naravno, Litt možda ima pravo. Možda će super-inteligentni AI sustavi doista uskoro postojati (premisa je dosta osnažena 6. listopada). No, postoje ozbiljni znanstveni i tehnički izazovi koji se često podcjenjuju:

• Nedostatak robusne generalizacije. Današnji modeli su izvrsni u prepoznavanju obrazaca, ali slabi u konceptualnim probojima koji zahtijevaju razumijevanje.
• Problem verifikacije. Čak i ako model proizvede točan dokaz, često nije jasno zašto je dokaz točan, niti može li pridonijeti razumijevanju dokazanoga.
• Krhkost modela. Modeli mogu biti “nadljudski” u jednoj domeni, a potpuno bespomoćni u drugoj. To je poznato kao jagged intelligence problem.

Već smo rekli da Litt smatra da su ciljevi matematike:

1. Proizvoditi i razumjeti visokokvalitetnu matematiku.
2. Proizvoditi visokokvalitetne matematičare.

Distinkcija između subjektivnih (razumijevanje) i socijalnih (prenošenje znanja) ciljeva je korisna. Litt s pravom tvrdi da su ti ciljevi nedostatno “operacionalizirani kroz dokazivanje teorema” i to naziva nepotpunom operacionalizacijom. No, Litt ne nudi alternativnu operacionalizaciju. Kaže da ne bismo trebali samo dokazivati teoreme, ali onda predlaže da se doktorat dodjeljuje na temelju “rigorozne obrane” — što je opet (usmena) forma dokazivanja. Osim toga, usmena obrana je subjektivna. Dva ispitivača mogu imati različite kriterije za “razumijevanje”. Pisana teza je, ako ništa drugo, javni i provjerljivi dokument. Ako ga zamijenimo usmenim ispitom gubimo transparentnost i mogućnost naknadne provjere. Da ne govorimo o tome da student može naučiti obraniti temu, a da je zapravo ne razumije – to je poznato svakome tko je bio s bilo koje strane usmenih ispita. Litt to ne adresira. Njegov prijedlog je manje radikalan nego što se čini.

Litt dalje piše: “Ako se matematički problem može riješiti po cijeni fine večere, trebali bismo biti oduševljeni.” Metafora je privlačna, ali opasna. Implicira da je matematika roba koja se može kupiti za novac. To mnogi matematičari odbijaju prihvatiti ne zato što su protiv AI-ja, već zato što smatraju da vrijednost matematike nije tržišna. Kao što je dobro napisao jedan komentator: “Pa, sve ovisi o tome tko se nalazi s druge strane te transakcije! Rado bih počastio večerom prijatelja i koautora koji mi je pomogao postići dobar rezultat. No, bismo li doista trebali biti „oduševljeni” davanjem novca korporacijama koje se bave izvlačenjem rente, a za koje imamo razloga vjerovati da ne mare ni za matematiku ni za matematičare?”

Littova metafora ignorira eksternalije. Ako AI kompanije “rješavaju” matematičke probleme, čine to radi profita a ne radi matematike. To može iskriviti prioritete discipline i stvoriti ovisnost o korporativnim interesima.

Litt gleda matematiku kao autonomnu disciplinu koja se može prilagoditi novoj stvarnosti neovisno o širim društvenim i ekonomskim silama. Ali matematika je ugrađena u institucije (sveučilišta, agencije za financiranje, izdavačke kuće) koje su podložne političkim i ekonomskim pritiscima. Taj prigovor iznose mnogi komentatori („javnost možda neće htjeti financirati matematiku ako AI može riješiti njene probleme“, „mladi možda neće htjeti ući u profesiju koja se doima kao exegesis of machine content “, „sveučilišta će se možda restrukturirati prema primijenjenim područjima“, itd). Litt to ne adresira. Njegov esej je apolitičan u najgorem smislu: pretpostavlja da se institucije mogu reformirati iznutra, bez obzira na vanjske pritiske.

Litt predlaže intervjue za doktorski studij, kulturu seminara, nagrađivanje vrijednih istraživačkih programa. Prijedlozi su razumni, ali nedovoljno konkretni. Koje ćemo kriterije koristiti? Kako ćemo mjeriti “vrijednost istraživačkog programa”? Ili još problematičnije. Kako ćemo znati što je “visokokvalitetna matematika”? Kako ćemo mjeriti “razumijevanje”? Na ta pitanja esej ne odgovara. Litt ne ulazi u te detalje. Njegov esej je dijagnoza bez recepta — dobro opisuje problem, ali ne nudi provediva rješenja.

Na kraju, valja primijetiti da Littov optimizam nije neutralan. On piše iz pozicije nekoga tko je već prihvatio AI kao neizbježnost i sada traži način da se s tim pomiri. To je legitimna pozicija, ali nije jedina. Oni koji su pesimistični ne pišu iz straha ili nostalgije, već iz opravdane zabrinutosti da se profesija mijenja na način koji je nepovratan i možda nepoželjan. Litt ih uglavnom ignorira ili ublažava njihove brige. Unatoč kritikama, Littov esej je važan jer:

• Iskreno postavlja pitanje – što je matematika ako AI može “riješiti” njene probleme? To je pitanje koje se mnogi boje postaviti.
• Predlaže konkretne promjene – doktorat kao obrana, intervjui, seminari; to su koraci u pravom smjeru.
• Ne prezire one koji ne koriste AI – Litt ostavlja prostor za pluralizam.
• Poziva na razgovor – esej je poziv na dijalog, a ne dogmatski manifest.

Littov esej je plemenit u namjeri, ali slabiji u izvedbi. Njegova vizija budućnosti matematike je optimistična, ali nedorečena. Njegovi prijedlozi su razumni, ali nekonkretni. Njegova analiza je oštra, ali nedovoljno politička. Najveći je problem eseja to što ne uzima ozbiljno mogućnost da je matematika, kakvu poznajemo, ugrožena. Litt pretpostavlja da će se profesija moći prilagoditi, ali ne pokazuje kako, a ni zašto bi se to trebalo dogoditi. Ako je Litt u pravu, matematika će se promijeniti. Ako nije, možda će se promijeniti još više. U oba slučaja, njegov esej je vrijedan čitanja – ne kao recept, već kao poziv na razmišljanje.

Zaključak

Eseja Daniela Litta i rasprava koja mu je uslijedila otkriva dubok rascjep u matematičkoj zajednici. S jedne strane stoje optimisti, koji vide AI kao oslobođenje i početak zlatnog doba matematike. S druge strane su pesimisti, koji vide AI kao egzistencijalnu prijetnju profesiji, institucijama i samom smislu bavljenja matematikom.

1. Temeljne teze optimista

Optimisti tvrde da AI neće uništiti matematiku, već će je osloboditi. Oslobađanje se sastoji u tome da će se matematičari moći posvetiti dubljim, konceptualnijim i kreativnijim aspektima svog rada, dok će rutinske zadatke (dokazivanje lema, pretraživanje literature, formalizacija) preuzeti strojevi.

Ključna premisa: matematika nije samo dokazivanje teorema. Ako je cilj razumijevanje, a ne samo istinitost, tada AI ne može zamijeniti ljude — može im samo pomoći. Optimisti tvrde da je zaliha otvorenih problema beskonačna. Svaki odgovor rađa nova pitanja. Nema opasnosti da će matematika “presušiti” – naprotiv, AI će ubrzati otkrivanje novih problema. Optimisti vide matematiku tek kao prvi val koji će se proširiti na sve znanosti. AI će omogućiti da se rješavaju problemi koji su nekada bili preskupi ili bi predugo trajali za ljudske istraživače.

Zato optimisti predlažu novu podjelu rada:

Zadatak	Tko ga obavlja
Rutinsko dokazivanje.	AI
Pretraživanje literature.	AI
Formalizacija, npr. u Leanu.	AI
Postavljanje pitanja.	Ljudi
Razumijevanje.	Ljudi
Poučavanje.	Ljudi
Izgradnja teorija.	Ljudi + AI

Optimisti ukazuju na analognu činjenicu da šah nije umro zbog Stockfisha – naprotiv, šah je postao popularniji nego ikad i isto će se dogoditi s matematikom. Optimisti ne vide sukob između korištenja AI-ja i autentičnog matematičkog razmišljanja. AI je alat poput olovke i papira – pomaže, ali ne misli umjesto nas.

2. Temeljne teze pesimista

Pesimisti tvrde da AI neće osloboditi matematiku, već je uništiti – ne u smislu da više neće biti matematičkih rezultata, već u smislu da će ljudsko razumijevanje matematike biti marginalizirano, a profesija kao društvena institucija oslabljena ili ugašena. Ključna je premisa: matematika je društvena praksa, a ne samo skup istinitih tvrdnji. Ako se ta praksa razori, matematika prestaje biti ono što jest.

Pesimisti tvrde da motivacija nije samo intelektualna – ona je egzistencijalna. Ako netko drugi (AI) može riješiti problem, zašto se truditi? Ako je rezultat “kupljen” za cijenu večere, gdje je ponos i radost stvaranja? Mladi ljudi neće htjeti ući u profesiju koja se doima kao exegesis of machine content. To će dovesti do demografske krize u matematici — manje studenata, manje doktoranada, manje profesora. Javnost neće htjeti financirati matematiku ako AI može “riješiti” probleme. Zašto plaćati matematičare ako chatbot to može besplatno? To će dovesti do kolapsa sveučilišnih odjela za matematiku. Pesimisti također drže da će se kvaliteta matematike srozati jer će AI generirati ogromne količine sloppy radova koji će preplaviti časopise, arhive i konferencije. Matematika će se utopiti u moru nekvalitetnih rezultata.

Zato pesimisti smatraju da matematičari ne smiju pristati na kompromis s AI-jem. Ako pristanu, izgubit će autonomiju, dignitet i smisao svoje profesije. Bolje je otići nego pristati na “distopiju”. Osim toga institucije nisu dovoljno agilne da se prilagode brzini promjene. Dok se sveučilišta, časopisi i agencije za financiranje dogovore o reformama, AI će već promijeniti pravila igre. Profesija će se raspasti prije nego što se uspije reformirati.

Unatoč dubokim razlikama, optimisti i pesimisti oko nečega se i slažu:

Točka slaganja	Optimisti	Pesimisti
AI će promijeniti matematiku	Da, nabolje	Da, nagore
Sadašnje institucije su neodržive	Da, treba ih reformirati	Da, ali reforma je nemoguća
Mladi su ključni	Da, treba ih privući	Da, treba ih zaštititi
Razumijevanje je važno	Da i AI pomaže razumijevanju	Da, ali AI ga uništava
Matematika nije samo dokazivanje	Da i to je prilika	Da i to je prijetnja

No, oko mnogih pitanja se razilaze:

Pitanje	Optimisti	Pesimisti
Hoće li AI biti bolji od ljudi?	Da, ali to je dobro	Da i to je katastrofa
Hoće li mladi ući u profesiju?	Da, ako se profesija reformira	Ne, jer profesija gubi smisao
Hoće li javnost financirati?	Da, ako pokažemo vrijednost	Ne, jer će AI biti “dovoljno dobar”
Može li se problem regulirati?	Ne, i ne treba	Da, i treba
Je li matematika roba?	Djelomično, i to je ok	Ne, i to je uvreda
Je li “cijena večere” dobra?	Da, trebamo biti oduševljeni	Ne, to je poniženje
Hoće li biti zlatno doba?	Da, već je počelo	Ne, dolazi mračno doba

Jedan od najzanimljivijih sukoba tiče se kvalitete AI-generirane matematike. Optimisti tvrde da je AI dovoljno dobar i da će se poboljšavati. Pesimisti tvrde da je AI sloppy — da proizvodi rezultate koji su formalno točni, ali bez razumijevanja. Razrješenje ovog sukob je možda ključno. Hoće li AI biti sloppy ili će biti dovoljno dobar? Odgovor na to pitanje određuje hoće li profesija preživjeti.

Neki pokušavaju naći srednji put između optimizma i pesimizma. Sam Daniel Litt piše: “Mislim da u ovom svijetu ima mjesta i za matematičare koji su, poput mene, oduševljeni umjetnom inteligencijom, i za one koji je ne koriste.” Ovaj pluralizam je privlačan, ali pesimisti ga odbacuju: ako AI proizvodi sloppy matematiku, pluralizam nije moguć — jer će sloppy matematika preplaviti sve.

Važno je razumjeti da se optimisti i pesimisti ne razlikuju samo u predviđanjima. Razlikuju se u vrijednostima.

Vrijednost	Optimisti	Pesimisti
Efikasnost	Visoko je vrednuju	Nisko je vrednuju
Razumijevanje	Važno, AI mu pomaže	Ključno, AI ga uništava
Autonomija	Manje važna	Ključna
Prestiž	Manje važan	Ključan
Zajednica	Važna, ali se mijenja	Ključna, ali se raspada
Smisao	AI oslobađa za dublji smisao	AI uništava smisao

Objema stranama zajednički je strah. Optimisti se boje da će matematika propustiti priliku. Pesimisti se boje da će matematika izgubiti dušu. Tko je u pravu? Možda oboje. Možda će AI osloboditi matematiku za one koji se prilagode, a uništiti je za one koji se ne prilagode. Možda će doći zlatno doba za matematiku, ali mračno doba za matematičare. Kako god bilo, rasprava je tek počela i treba je nastaviti.

---

Malo konkretizacije

Evo i konkretnijih opaski za matematičare (a i ostali će dobiti neki dojam o problemima u suživotu matematike i umjetne inteligencije). Šokirani brzinom i načinom na koji je OpenAI 6. listopada 2026. godine na GitHubu objavio 722 znanstvena rada raspoređena u 372 grupe rezultata, matematičari su se suočili s nezapamćenim organizacijskim izazovom. Budući da su radovi pisani u gustom i dosta neobičnom stilu koji stručnjaci opisuju kao da ih je “pisao netko na psihodeličnim drogama”, matematička zajednica morala se hitno organizirati kako bi provela recenziju i zadržala kontrolu nad strukom. To se trenutno odvija kroz tri ključne institucije.

1. AGMAI

Kako bi se stvorio službeni most između AI kompanija i akademske zajednice, još i prije 6. listopada 2026., osnovana je nezavisna matematička organizacija Advisory Group on Mathematics and Artificial Intelligence (AGMAI), pod okriljem Institute for Advanced Studies (IAS) u Princetonu (gdje su nekada stolovali i duge razgovore vodili Einstein i Gödel). To tijelo (koje čini devet istaknutih svjetskih znanstvenika) donijelo je stroge smjernice za ponašanje tehnoloških laboratorija.

Iako je OpenAI tvrdio da je uvažio savjete AGMAI-ja, organizacija ih je javno prozvala jer su prekršili njihovu glavnu preporuku: da prestanu testirati napredne matematičke probleme na zatvorenim, komercijalnim i tajnim modelima. AGMAI zahtijeva potpunu transparentnost oko promptova, metodologije i utrošene računalne snage.

2. AHM

Kao izravna reakcija na OpenAI-jev “desant” na GitHub, osnovana je nova, radikalnija organizacija pod nazivom Association for Human Mathematics (AHM). Ona je odmah objavila oštar prosvjedni proglas koji je javno podržao i podijelio i vodeći svjetski matematičar Terence Tao (inače i član AGMAI-ja).AHM optužuje tvrtku za demonstraciju gole korporativne moći i ignoriranje ljudskog doprinosa.

Pozivaju na potpuni bojkot recenziranja OpenAI-jevih radova dok god su oni strukturirani tako da guše ljudsko razumijevanje i služe samo skupljanju bodova za investitore.

3. Crowdsourcing i decentralizirana provjera

Dok jedan dio zajednice poziva na bojkot, drugi je dio zaključio da se radovi ne mogu ignorirati te su pokrenuli decentraliziranu, masovnu akciju provjere (crowdsourcing). Matematičari i programeri masovno preuzimaju OpenAI-jev repozitorij (openai/math) kako bi u VS Code-u i preko lokalnih Lean prevoditelja pokrenuli provjere koda. Na platformi MathOverflow pokrenute su specijalizirane, kolaborativne rasprave. Umjesto da pojedinci čitaju stotine stranica, dokazi su “razlomljeni” prema područjima (algebra, logika, geometrija). Stručnjaci za pojedina područja preuzimaju na sebe zadatak da “prevedu” računalne koncepte i provjere jesu li OpenAI-jevi agenti doista dokazali ono što tvrde ili je u pitanju problem pogrešnog prijevoda u Lean (mismatch).

Matematička zajednica je, dakle, organizirala obrambene mehanizme. AGMAI, AHM i forumi šalju poruku: kompanije mogu generirati dokaze, ali matematičari tek trebaju ustanoviti što je tu točno, vrijedno i smisleno.

Da bismo bolje razumjeli u čamu je problem moramo razumjeti ulogu Lean-a (interaktivnog dokazivača teorema i programskog jezika) u sustavima umjetne inteligencije. Ona je ključni element automatske verifikacije i potvrde točnosti složenih matematičkih tvrdnji koje generiraju napredni AI modeli. OpenAI koristi Lean prvenstveno kao računalni filtar za provjeru logičkih koraka u masovnim izdanjima svojih matematičkih istraživanja. Nakon što je njihov interni model (razvijan pod kodnim imenima poput Astra) generirao rješenja za stotine matematičkih problema, Lean je upotrijebljen za formalnu provjeru ključnih rezultata unutar objavljenog repozitorija.

Evo detaljnijeg pregleda kako OpenAI koristi Lean i zašto je ključan za budućnost AI dokaza.

Najveći problem s naprednim AI modelima (poput GPT serije) u matematici je to što mogu generirati tekst koji naizgled zvuči točno i uvjerljivo, ali sadrži skrivene logičke pogreške. Taj problem bi trebao riješiti Lean.

• AI model najprije generira dokaz na prirodnom jeziku (engleskom), a zatim drugi sustav prevodi taj dokaz u strojno čitljiv kod unutar jezika Lean.
• Ako Lean prihvati kod i uspješno ga kompajlira bez pogrešaka, dokaz je matematički 100% valjan unutar zadanih pravila. OpenAI je tako formalizirao stotine svojih glavnih rezultata kako bi dokazao njihovu točnost.

No, znanstvena zajednica (kroz platforme poput arXiv-a) ističe ključni problem u načinu na koji se OpenAI koristi tim alatom. Činjenica da je Lean uspješno verificirao neki kod ne znači nužno da je početni dokaz pisan na engleskom jeziku bio savršen. Ponekad AI tijekom prevođenja u Lean “tiho ispravi” greške ili nesvjesno oslabi početnu tvrdnju kako bi je računalo lakše prihvatilo. To je problem poznat pod nazivom Semantic Faithfulness. Zato stručnjaci naglašavaju da oznaka “Lean Verified” i dalje zahtijeva ljudsku provjeru samog procesa prijevoda (autoformalizacije) kako bi se osiguralo da računalo i čovjek pričaju o potpuno istoj matematičkoj teoriji. Dakle, kada Lean potvrdi da je dokaz 100% matematički točan, proces još nije gotov. Ljudski matematičari moraju prekontrolirati jesu li AI definicije u Lean-u oslabile izvorni problem.

• Primjer: Ako je model trebao dokazati teorem za sve realne brojeve, a u Lean kodu je greškom napisao “za sve pozitivne cijele brojeve”, Lean će dokazati taj lakši teorem bez greške. Zato ljudi na kraju moraju potvrditi da prevedeni teorem uistinu znači isto što i izvorni.

Evo i nekih konkretnih slučajeva.

Kada je OpenAI lansirao svoja 722 matematička rada, samo je oko 42% rezultata bilo potpuno verificirano Lean-om. Manje od 24 sata nakon objave, OpenAI je bio prisiljen povući 3 rada i prepraviti još 14 drugih.

Najsuptilnija i najopasnija greška je u autoformalizaciji, tj. u gubitku vjernosti prijevoda (Semantic Faithfulness). Ona se pokazala kod ranijeg OpenAI-jevog dokaza za Navier-Stokesove jednadžbe (što je najvažniji rezultat OpenAi-ja, jer se radi o milenijskom problemu). Matematičari su analizom otkrili da dokaz napisan na engleskom jeziku (za ljude) i dokaz napisan u Lean kodu (za računalo) nisu govorili o istoj stvari. Lean je potvrdio da je kod koji mu je zadan 100% točan. Međutim, AI model je tijekom prevođenja u kod ublažio početne pretpostavke teorema kako bi ga Lean lakše prožvakao. Lean je tako uspješno dokazao verziju problema koju mu je AI servirao, ali ta verzija nije odgovarala stvarnom problemu.

Lean ne može provjeriti je li problem dobro preveden, on samo provjerava slijedi li prevedeni formalizirani zaključak iz prevedenih formaliziranih premisa. AI modeli često iskorištavaju ovu slijepu pjegu kroz:

• Trivijalizaciju tvrdnji: Na primjer, ako AI definira skup objekata kao “prazan skup” (jer je napravio grešku u kodu), Lean će bez problema dokazati bilo koje svojstvo za elemente toga skup (jer ih prazan skup nema). Dokaz prolazi s ocjenom “Uspješno”, iako je matematički beskoristan.
• Zlouporabu sorry i axiom naredbi: Ako AI krivo poveže datoteke i unese nedokazanu pretpostavku kao aksiom, Lean će pretpostaviti da se radi o aksiomu i proglasiti dokaz valjanim, ne uočavajući činjenicu da ključni korak zapravo nedostaje.

Zbog ovakvih propusta, matematičari oštro kritiziraju OpenAI, navodeći da masovno “zatrpavanje” GitHub-a neprovjerenim radovima stvara golem kaos u kojem ljudi moraju trošiti vrijeme kao “kod-revizori” za umjetnu inteligenciju umjesto da se bave matematikom.

To ne znači da AI dokazi katkada nisu nevjerojatno inovativni. Na primjer, jedan od dokaza objavljenih 6.10. 2026. daje negativno rješenje 10. Hilbertovog problema za racionalne brojeve (postoji li opći algoritam za odluku ima li diofantska jednadžba racionalna rješenja). Originalni problem za cijele brojeve riješen je još 1970. i svi pokušaji u sljedećih više od pola stoljeća išli su za time da cijele brojeve definiraju $\Sigma$ formulom u području racionalnih brojeva, što bi problem svelo na onaj već riješeni 1970. No, nije bilo pomaka.

AI dokaz je krenuo sasvim drugim putem. On konstruira elementarno (nestandardno) proširenje polja racionalnih brojeva unutar kojeg se pojavljuju “lažni cijeli brojevi” (nestandardni elementi koji se ponašaju poput cijelih brojeva). Da bi se spriječilo da konačni testovi prihvate te lažne elemente kao stvarna rješenja, elementi prstena se preslikavaju u točke fiksirane cikličke podgrupe eliptičke krivulje ranga 1. Višekratnici točaka vjerno kodiraju zbrajanje, dok se množenje kontrolira lokalnim usporedbama pomoću eliptičkih logaritama.

Ključni element dokaza je usporedba asimptotskog rasta. Dok s jedne strane aritmetička veličina (informacijski otisak) raste linearno kada „lažni broj“ ne rješava polinom, na strani eliptičke krivulje koordinate rastu kvadratno s tim „lažnim brojem“. Kontradikcija između linearne i kvadratne granice prisiljava „lažne brojeve“ da kolabiraju natrag u standardne, što problem svodi na onaj riješen 1970. godine. Naravno, sve to treba provjeriti, ali već je sama ideja kojom je AI pristupio problemu briljantna.

AI dokazi su tu, ali tu su i matematičari. Da evaluiraju te dokaze i da potaknuti njima (ili ne) i dalje stvaraju novu matematiku.