Teoretičari brojeva zabrinuti su da je sva matematika dosad pogrešna

Dešava se proboj različitih softvera u polje teorijske matematike. Neki od najvećih umova ovog polja, velika imena poznata po svojoj pouzdanosti, počinju da koriste softvere kako bi im pomogli da razumeju i verifikuju određene dokaze.

Kevin Bazard, teoretičar brojeva i profesor teorijske matematike na Imperial koledžu u Londonu, veruje da je vreme da se stvori nova oblast matematike posvećena kompjuterizaciji dokaza. Neki od najvažnijih dokaza postali su toliko kompleksni da praktično ne postoji ljudsko biće na planeti koje može da ih razume u svim pojedinostima i detaljima, a kamoli da ih verifikuje. On se plaši da su mnogi dokazi, široko prihvaćeni kao tačni, možda zapravo pogrešni. Potrebna je pomoć.

Šta je dokaz? Dokaz je demonstracija istinitosti matematičkog iskaza. Dokazivanjem i učenjem novih tehnika dokazivanja razvija se bolje razumevanje matematike, što se onda prenosi i na druga polja.

Kako bismo dobili nešto što je dokaz, moramo početi od nekih definicija. Na primer, definišimo set brojeva kakvi su intidžeri, svi celi brojevi od minus beskonačno, do plus beskonačno. Ovakav set brojeva zapisujemo kao: … , -2, -1, 0, 1, 2, … Dalje, postavljamo teoremu, na primer, da ne postoji jedan pojedinačni najveći intidžer. Dokaz se, dalje, sastoji od logičkog rasuđivanja koje pokazuje da li je teorema tačna ili netačna, u ovom slučaju - tačna. Logički koraci u ovom dokazu zasnivaju se na drugim, ranije utvrđenim istinama, za koje smo već utvrdili da su prihvaćene i dokazane. Na primer, činjenica je da je broj jedan manji od broja dva.

Novi dokazi koje prave profesionalni matematičari obično se zasnivaju na velikom broju ranijih rezultata koji su već negde objavljeni i shvaćeni. Ipak, Bazard kaže da u mnogim slučajevima, ranije utvrđeni dokazi korišćeni su da se izgrade novi dokazi, zapravo očigledno nisu shvaćeni. Na primer, postoji značajan broj radova koji otvoreno citiraju neke i dalje ne objavljene radove. I ovo brine Bazarda.

“Zabrinut sam da je sva objavljena matematika pogrešna, i to iz razloga jer matematičari ne proveravaju detalje, a već sam iskusio da vidim da su pogrešili,“ rekao je Bazard za Motherboard dok je prisustvovao desetoj Interaktivnoj konferenciji posvećenoj dokazivanju teorema u Portlandu, u Oregonu, gde je držao govor na otvaranju.

"Mislim da postoji šansa da su neki od naših najvećih zamaka zapravo izgrađeni na pesku,“ napisao je Bazard u svojoj prezentaciji. “Ipak, mislim da ta šansa nije velika.“

Nova matematička saznanja trebalo bi da budu dokazana od osnova. Svaki korak mora biti proveen, ili u najmanju ruku ispraćen određenim objašnjenjem. Sa druge strane, postoje eksperti i ljudi koji su već jako dugo članovi matematičke zajednice koji obezbeđuju pouzdane smernice kada se radi o pitanjima šta je tačno, a šta ne. Ukoliko neki od tih eksperata citira neki rad, ili ga koristi u svom sopstvenom radu, onda taj rad verovatno ne mora da bude dalje proveravan, ili bar tako mislimo.

Bazard ukazuje na to da je savremena matematika postala previše zavisna od toga šta kažu eksperti, baš zato što su rezultati postali toliko kompleksni. Novi dokaz može uključivati preko dvadeset citiranih radova, a samo jedan od tih radova može se sastojati iz preko hiljadu stranica razjašnjavanja različitih pojmova. Ukoliko neki cenjeni senior matematičar citira rad od hiljadu stranica, ili ga koristi na neki drugi način, onda mnogi drugi matematičari mogu samo pretpostaviti da je taj rad od hiljadu stranica (kao i taj novi dokaz) tačan, kao i da nema potrebe to dalje proveravati. Ipak, matematika bi trebalo da bude univerzalno proverljiva, a ne zavisna od mišljenja nekoliko eksperata.

Ovakva prevelika zavisnost od ovakvih eksperata dovodi do poteškoća da se shvati šta je istina. Dokaz Fermaove Poslednje Teoreme, koja je nastala 1637. i koja je u jednom periodu u Ginisovoj knjizi rekorda bila zabeležena kao “najkomplikovaniji matematički problem,“ objavjena je devedesetih. Bazard kaže da niko zapravo nije u stanju da je u potpunosti razume, kao ni da potvrdi da li je tačna ili ne.

"Ne verujem da postoji bilo koji čovek, živ ili mrtav, koji poznaje sve detalje dookaza Fermatove poslednje teoreme. Ipak, zajednica ovaj dokaz prihvata bez obzira na to,“ napisao je Bazard u svojoj prezentaciji. Zbog toga što “su priznati eksperti priznali ovaj dokaz kao dobar.“

Pre nekoliko godina, Bazard je gledao govore matematičara seniora Tomasa Hejlesa i Vladimira Voevodskog koji su mu predstavili softver za verifikaciju koji postaje poprilično dobar. Uz upotrebu ovog softvera, dokazi mogu biti sistematički verifikovani od strane kompjutera, što ovaj zadatak skida sa ramena priznatih eksperata i onemogućava polemiku o statusu istinitosti dokaza.

Kada je Bazard počeo da koristi ovaj softver za verifikaciju dokaza koji nosi naziv Lean, više nije mogao da prestane da ga koristi. Ne samo što je ovaj softver omogućio da se dokazi verifikuju bez sumnje verodostojnost ishoda, već ovaj softver promoviše perspektivu da matematika treba biti jasna i izbegava mogućnost pogreške.

“Shvatio sam da kompjuteri jedino mogu da prihvate inpute u veoma određenoj formi, što je moj najdraži način razmišljanja kada se radi o matematici,“ rekao je Bazard. “Zaljubio sam se, osećao sam se kao da sam pronašao srodnu dušu. Pronašao sam nešto što ima pogled na matematiku isti kao što sam i ja razvijao.“

Kako bi verifikovao svoj dokaz, korisnik softvera Lean mora formalizovati dokaz, ili ga konvertovati iz ljudskog jezika i simbola u programski jezik koji ovaj softver koristi. Korisnik takođe mora formalizovati svaku poddefiniciju i dokaz na kome se zasniva njegov novi rad. I iako ovaj proces konverzije zahteva iscrpan rad, Lean izgleda može da se nosi sa bilo kojom matematikom koju je Bazard uneo, za razliku od ostalih programa koji za cilj imaju verifikaciju dokaza.

Lean je privukao pažnju zajednice matematičara, koja sve više raste, posebno kada se radi o predavačima. Džeremi Eviged je profesor na Karnegi Melon, i specijalizuje se za teoriju dokaza. I Eviged i Bazard počeli su da koriste Lean na uvodnim kursevima na koledžu gde se izučavaju dokazi. Ovaj softver proverava svaki red dokaza i daje povratne informacije, što dosta pomaže studentima.

I iako je Eviged uzbuđen zbog činjenice da se zajednica zainteresovala za ovaj softver, on upozorava da ovu tehnologiju i dalje treba unaprediti. Ovakvi softveri zahtevaju korišćenje koje traje značajni vremenski period. “Ovo polje izučavanja postoji već nekoliko decenija, i stanje je sve bolje, pa ipak, i dalje nismo na nivou na kome bismo želeli da budemo,“ rekao je on.

Bazard smatra da, ukoliko se ovi izazovi prevaziđu, ovaj softver može imati širu primenu nego samo na verifikaciju dokaza. Na primer, tu je problem pretrage. Ogromne količine novih rezultata objavljivane su svake godine, i to velikom brzinom, što pretragu kroz ovakve dokaze čini veoma važnom.

Hejls i Bazard ukazali su na to da ukoliko bi svi apstrakti ovih novih radova bili uneti u softver Lean, bilo koji matematičar mogao bi pretražiti bazu podataka ovih apstrakta u potrazi za konkretnim matematičkim objektom unetim u softver, i saznati sve što je do sada o njemu poznato. To bi, do neke mere, moglo zameniti dosadašnju zavisnost od onoga što je pohranjeno u mozgovima matematičkih eksperata.

Istraživači koji se bave kompjuterskim naukama mogli bi ovakve baze podataka iskoristiti kao osnovu za trening veštačke inteligencije. Upravo iz razloga što će ovakvi rezultati u ovoj bazi podataka biti definisani preciznim jezikom koji koristi softver Lean, programima će biti značajno olakšano da uče iz njega, u poređenju sa rezultatima koji su zapisani idiosinkratičkim jezikom.

I na samom kraju, istraživači u kompjuterskim naukama voleli bi da stvore opšti automatizovani dokazivač teorema, softverski sistem koji će moći da stvara sopstvene dokaze, kao i da sam radi matematiku. Automatizovani dokazivači koji bi trebalo da odluče da li je neki dokaz istinit počivaju na istoj tehnologiji kao i Lean. Sve šira upotreba ovog softvera mogla bi biti veoma važan formativni korak ka sveopštoj automatizaciji matematike.

U Helix Centru, na Menhetnu, u subotu petog oktobra održaće se okrugli sto, diskusija koja za tomu ime automatizaciju matematike, a biće uživo strimovana na njihovom Jutjub kanalu, kao i na njihovom vebsajtu. Majkl Heris, profesor matematike na Kolumbija Univerzitetu i Bazardov kolega, takođe će učestvovati na ovom forumu.

Heris je zabrinut za to da kompjuterski naučnici i tehnološke kompanije koje žele da automatizuju matematiku nemaju iste motive kao matematičari. Kompjuterski naučnici, na primer, žele da koriste tehnologiju koja pokreće Lean kako bi utvrdili da programi ne baguju. Kompanije žele da povećaju profit. Matematičari poput Bazarda, sa druge strane, samo žele da rade matematiku.

“Ono što mogu da predvidim je da, ukoliko mudri ljudi poput Tomasa Hejlsa i Bazarda nastave da razmišljaju ovim putem, nešto interesantno će nastati iz toga; možda to neće biti veštačka inteligencija, ali će možda nastati mnoštvo novih grana matematike, ili potpuno novi način razmišljanja,“ rekao je Heris.

Ovaj članak prvobitno je objavljen na VICE US.