U polje matematičke teorije sve više ulaze razni softveri pa neki od najvećih matematičkih umova počinju ih koristiti kako bi im pomogli da razumiju i verificiraju određene dokaze. 

Kevin Buzzard, teoretičar brojeva i profesor teorijske matematike na Imperial Collegeu u Londonu, vjeruje da je vrijeme da se stvori nova grana matematike posvećena kompjutorizaciji matematičkih dokaza. Neki od najvažnijih postali su toliko kompleksni da praktično ne postoji ljudsko biće na planeti koje ih može razumijeti u svim pojedinostima i detaljima, a kamoli ih verificirati. On strahuje da su mnogi dokazi, općeprihvaćeni kao točni, možda zapravo pogrešni. Potrebna je pomoć, piše portal Vice. 

Umjetnost fraktala Postao je matematički genije nakon udarca u glavu

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

Da bismo dobili nešto što je dokaz, moramo početi od nekih definicija. Na primjer, definirajmo niz brojeva kakvi su svi cijeli brojevi od minus beskonačno, do plus beskonačno. Ovakav niz brojeva zapisujemo kao: ... , -2, -1, 0, 1, 2, ...

Dalje, postavljamo teorem, na primjer, da ne postoji jedan pojedinačni najveći cijeli broj. Dokaz se, dalje, sastoji od logičkog rasuđivanja koje pokazuje je li teorem točan ili netočan, a u ovom slučaju je točan. 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. Primjerice, činjenica da je broj jedan manji od dva.  

Novi dokazi koje izvode profesionalni matematičari obično se zasnivaju na velikom broju ranijih rezultata koji su već negdje objavljeni i shvaćeni. Ipak, Buzzard kaže da su u mnogim slučajevima, ranije utvrđeni dokazi korišteni da se izgrade novi dokazi, a zapravo očigledno nisu shvaćeni. Na primjer, postoji značajan broj radova koji otvoreno citiraju neke i dalje neobjavljene radove. I to brine Buzzarda.

“Zabrinut sam da je sva objavljena matematika pogrešna, i to iz razloga jer matematičari ne provjeravaju detalje, a već sam i sam iskusio i vidio da su pogriješili,“ rekao je Buzzard za Motherboardu dok je sudjelovao na desetoj Interaktivnoj Konferenciji posvećenoj dokazivanju teorema u Portlandu u Oregonu, gdje je držao govor na otvaranju.

Matematičar Istinita priča o genijalcu iz filma Good Will Hunting

"Mislim da postoji šansa da su neke od naših najvećih matematičkih kula izgrađene od pijeska Ipak mislim da ta šansa nije velika,“ napisao je Buzzard u svojoj prezentaciji.

"Nova matematička saznanja trebalo bi dokazivati od početka. Svaki korak moro bi se provjeriti ili u najmanju ruku ispratiti određenim objašnjenjem. Istovremeno, postoje eksperti koji su već jako dugo članovi matematičke zajednice i koji osiguravaju pouzdane smjernice kad je riječ o dvojbama što je točno, a što netočno.

Ukoliko neki od tih eksperata citira neki rad, ili ga koristi u svojem vlastitom radu, onda taj rad vjerojatno ne mora biti dalje provjeravan. Ili barem tako mislimo", govori Buzzard. 

Buzzard ukazuje na to da je suvremena matematika postala previše ovisna o tvrdnjama eksperata, baš zato što su razultati postali toliko kompleksni. NOvi dokaz može uključivati više od 20 citiranih radova, a samo jedan od njih može se sastojati od više od 1000 stranica objašnjenja različitih pojmova.

Matematika More, kopno... Ovo su najdulje ravne linije na Zemlji

Ukoliko neki cijenjeni sednior matematičar citira rad od tisuću stranica ili ga koristi na neki drugi način, onda mnogi drugi matematičari mogu samo pretpostavljati da je taj rad od 1000 stranica, kao i novi dokaz koji to objašnjenje koristi - u konačnici točan.

Kao i da nema potrebe to dalje provjeravati. Ipak, matematika bi trebala biti univerzalno provjerljiva, a ne zavisna od mišljenja nekoliko eksperata, smatra ovaj matematičar.

Ovakva prevelika ovisnost o takvim ekspertima dovodi do poteškoća da se shvati što je istina. Buzzard navodi primjer Fermatovog Posljednjeg teorema koji je nastao 1637. i proglašen je 'najkompliciranijim matematičkim problemom'. Bazard kaže da nitko zapravo nije u stanju u potpunosti ga razumijeti kao ni potvrditi je li točan ili ne. 

"Ne verujem da postoji bilo koji čovjek, živ ili mrtav, koji poznaje sve detalje dookaza Fermatoog Posljednjeg teorema a ipak je zajednica ovaj dokaz prihvatila samo zato jer su ga priznali poznati eksperti i rekli da je dobar", kaže Buzzard.  

Pre nekoliko godina, Bazard je gledao govore matematičara seniora Thomasa Halesa iVladimira Vevodskija  koji su mu predstavili prilično dobar softver uz pomoć kojeg kompjutor može sistematički verificirati dokaze, što ovaj zadatak skida sa ramena priznatih eksperata i onemogućava polemiku o istinitosti dokaza.

Ne samo što je ovaj softver omogućio da se dokazi verificiraju bez sumnje u vjerodostojnost, nego promovira perspektivu da matematika treba biti jasna i izbjegava mogućnost pogreške.

“Shvatio sam da kompjuteri jedino mogu prihvatiti inpute u vrlo određenoj formi što je i moj omiljeni način razmišljanja kad je riječ o matematici", kaže Buzzard o softveru Lean.

Milijuni 14 puta je osvojio jackpot - otkrio je kako pobijediti

Lean je privukao pažnju zajednice matematičara, koja sve više raste, posebno kad je riječ o predavačima. Koristi ga i profesor Jeremy Avigad s Carnegie Mellona i kažu da Lean provjerava svaki red dokaza i daje povratne informacije, što dosta pomaže studentima, ali kažu da još ima prostora za napredak i da ovaj softver zahtijeva dobre pripreme prije no što se u njega počnu unositi podaci.

U Helix Centru, na Manhattanu početkom listopada održao se i okrugli stol na temu automatizacije matematike na kojem su sudjelovali brojni profesori matematike s uglednih fakulteta. Michael Harris s Columbia University zabrinut je zbog toga što misli da informatički znanstvenici i tehnološke kompanije koji žele automatizirati matematiku nemaju iste motive kao i matematičari.

Kompjutoraši žele koristiti tehnologiju koja pokreće Lean kako bi utvrdili da programi nemaju bug i žele povećati profit, dok matematičari samo žele raditi matematiku.

“Ono što mogu predvidjeti je da, ukoliko mudri ljudi poput Thomasa Halesa i Buzzarda nastave razmišljati ovim putem, može iz toga nastati nešto zanimljivo. Možda to neće biti umjetna inteligencija, ali će nastati možda mnogo novih grana matematike ili potpuno novi način razmišljanja", kaže Harris.