Postoje neki prilično magloviti pojmovi u matematici o kojima može biti teško da se zamislite, ali značenje ‘jednako’ je ono za koje smo mislili da smo pokrili.
Ispostavilo se da se matematičari zapravo ne mogu složiti oko definicije šta dve stvari čini jednakim, a to bi moglo da izazove glavobolje kompjuterskim programima koji se sve više koriste za proveru matematičkih dokaza.
Ova akademska svađa traje decenijama, ali je konačno došla do vrhunca jer kompjuterski programi koji se koriste za ‘formalizaciju’ ili proveru dokaza moraju da imaju jasna, specifična uputstva; ne dvosmislene definicije matematičkih koncepata koji su otvoreni za tumačenje ili se oslanjaju na kontekst koji računari nemaju.
Britanski matematičar Kevin Buzzard sa Imperijal koledža u Londonu naišao je na ovaj problem kada je sarađivao sa kompjuterskim programerima, i to ga je navelo da ponovo razmotri definicije ‘ovo je jednako tome’, kako bi „osporio različite slogane o jednakosti koji razumno zvuče.
„Pre šest godina“, piše Buzzard u svom preprintu objavljenom na arKsiv serveru, „mislio sam da razumem matematičku jednakost. Mislio sam da je to jedan dobro definisan pojam… Onda sam počeo da pokušavam da radim matematiku na master nivou u kompjuterskoj teoremi dokazivača, i otkrio sam da je jednakost mnogo teži koncept nego što sam cenio.“
Znak jednakosti (=) sa dve paralelne linije koje elegantno predstavljaju paritet između objekata postavljenih sa obe strane, izumeo je velški matematičar Robert Rekord 1557. godine.
Isprva se nije uhvatio, ali je vremenom Rekordov briljantno intuitivni simbol zamenio latinsku frazu ‘aekualis’ i kasnije postavio temelje za kompjutersku nauku. Tačno 400 godina nakon njegovog pronalaska, znak jednakosti je prvi put korišćen kao deo kompjuterskog programskog jezika, FORTRAN I, 1957. godine.
Međutim, koncept jednakosti ima mnogo dužu istoriju, koja datira barem iz antičke Grčke. A savremeni matematičari, u praksi, koriste termin „prilično slobodno“, piše Buzzard.
U poznatoj upotrebi, znak jednakosti postavlja jednačine koje opisuju različite matematičke objekte koji predstavljaju istu vrednost ili značenje, nešto što se može dokazati uz nekoliko promena i logičkih transformacija sa jedne na drugu stranu. Na primer, ceo broj 2 može da opiše par objekata, kao i 1 + 1.
Ali druga definicija jednakosti se koristi među matematičarima od kasnog 19. veka, kada se pojavila teorija skupova.
Teorija skupova je evoluirala, a sa njom se proširila i matematička definicija jednakosti. Skup kao što je {1, 2, 3} može se smatrati ‘jednakim’ skupu kao što je {a, b, c} zbog implicitnog razumevanja zvanog kanonski izomorfizam, koji upoređuje sličnosti između struktura grupa.
„Ovi skupovi se međusobno poklapaju na potpuno prirodan način i matematičari su shvatili da bi bilo zaista zgodno da ih nazovemo jednakima“, rekao je Buzzard za Alek Vilkins iz Nev Scientist-a.
Međutim, uzimanje kanonskog izomorfizma da znači jednakost sada izaziva „neke prave nevolje“, piše Buzzard, za matematičare koji pokušavaju da formalizuju dokaze – uključujući decenijama stare temeljne koncepte – koristeći kompjutere.
„Nijedan od [računarskih] sistema koji do sada postoje ne obuhvata način na koji matematičari poput Grotendika koriste simbol jednakosti“, rekao je Bazar Vilkinsu, misleći na Aleksandra Grotendika, vodećeg matematičara 20. veka koji se oslanjao na teoriju skupova da bi opisao jednakost. .
Neki matematičari misle da bi trebalo samo da redefinišu matematičke koncepte da bi formalno izjednačili kanonski izomorfizam sa jednakošću.
Buzzard se ne slaže. On smatra da bi nepodudarnost između matematičara i mašina trebalo da podstakne matematičke umove da preispitaju šta tačno podrazumevaju pod matematičkim konceptima koji su temeljni kao što je jednakost kako bi kompjuteri mogli da ih razumeju.
„Kada je neko primoran da zapiše šta zapravo misli i ne može da se sakrije iza tako loše definisanih reči“, piše Buzzard. „Čovek ponekad otkrije da mora da radi dodatni posao, ili čak da preispita kako bi određene ideje trebalo da budu predstavljene.“
Istraživanje je objavljeno na arXiv.
