Ko matematikov več ne bo

Evolucija matematike je pokazala, da je svet številk in likov veliko bolj izmuzljiv in nedoločljiv, kot nam pravi intuicija

Evolucija matematike je pokazala, da je svet številk in likov veliko bolj izmuzljiv in nedoločljiv, kot nam pravi intuicija.

Klasična slika matematike, ki temelji na aksiomih, mnoštvu izrekov in previdno izbranih resnicah, ki jih v potu svojega obraza dokazujejo matematiki, se je v zadnjih dveh stoletjih pošteno nakrhala. Po odkritjih, da nekaterih aksiomov ne potrebujemo, da noben sistem aksiomov ne more biti popoln in da bodo vedno obstajale resnične, a nedokazljive izjave, v 21. stoletju računalniki grozijo, da bodo matematike preprosto – nadomestili.

Stari Grki niso bili prvi, ki so uporabljali matematiko. Pred njimi so že vsaj Egipčani, Mezopotamci, Babilonci in Sumerci računali, merili in opazovali zvezde. A stari Grki posebno mesto zasedajo zato, ker so prvi sistematično definirali sistem aksiomov in izpeljevanja izrekov v matematiki.

Evklid je napisal več knjig, najbolj znani so Elementi, ki so na Zahodu po Svetem pismu druga najbolj citirana knjiga. Čeprav gre v glavnem za pregled dosežkov starogrških matematikov iz teorije števil, geometrije in algebre, je delo ključno zaradi strukturiranosti. Prvikrat uporabi aksiomatsko metodo, pri kateri se iz osnovnih predpostavk z logičnim sklepanjem izpeljujejo trditve. Še danes matematika deluje tako. Evklid je ločil aksiome in postulate. Prvi so splošna pravila, ki bi veljala v katerikoli znanstveni vedi, drugi pa posebna pravila v zvezi s snovjo in kot taka na primer definirajo vrsto matematike. V modernem matematičnem jeziku bi oboje imenovali aksiomi, saj njihove pravilnosti ne dokazujemo, temveč jo privzamemo kot dano resnico.

Prvi štirje Evklidovi postulati so očitni: med dvema točkama je možno potegniti premico, daljico lahko podaljšamo v premico, možno je konstruirati krog s središčem v točki in znanim polmerom, vsi pravi koti so med seboj enaki. Peti postulat pa v svojem bistvu pravi, da lahko skozi dano točko k obstoječi premici vedno potegnemo eno in samo eno vzporednico (formulacija Johna Playfaira iz 18. stoletja). Znameniti peti postulat ni niti samoumeven niti očiten. Morda se na prvi pogled zdi, da bi tako moralo veljati, a to je v matematiki slab argument. Dva tisoč let so matematiki poskušali streti ta oreh na dva načina: morda je ta postulat možno izpeljati iz preostalih postulatov ali pa ga lahko spremenimo in pokažemo, da je nastala geometrija protislovna. Zaman.

Da tega postulata ni možno izpeljati iz prvih štirih, nima posebnih posledic; očitno je neodvisen od njih. Revolucionarno v matematiki pa je bilo odkritje, da ga lahko spremenimo, pa se logična konsistentnost geometrije ne podre. Poskusov je bilo več, toda prva sta to neodvisno drug od drugega rigorozno dokazala ruski matematik Nikolaj Ivanovič Lobačevski leta 1829 in madžarski matematik Janos Bolyai leta 1832. Če skozi dano točko lahko k premici potegnemo neskončno vzporednic, dobimo neevklidsko hiperbolično geometrijo (geometrija Bolyai-Lobačevskega). Nemški matematik Bernhard Riemann pa je leta 1854 pokazal še, da obstaja tudi druga skrajnost. V eliptični geometriji (Riemannova geometrija) k premici skozi dano točko v splošnem ne moremo potegniti nobene vzporednice.

Riemann je v resnici pokazal nekaj zelo zemeljskega – najprimitivnejši primer eliptične geometrije je sferična geometrija, ki opisuje površje Zemlje. V sferični geometriji je posplošitev premice geodetka, tj. najkrajša pot med dvema točkama po velikem krogu. Vsi veliki krogi na Zemlji se paroma dvakrat sekajo – vzporednic ni.

Gödel pretrese matematiko

Vse od grških začetkov so matematiki hrepeneli po elegantnosti, ki izvira iz ustroja matematike. Temelji naj na čim manjšem številu osnovnih neizpodbitnih, nedokazljivih in konsistentnih resnic, tako da izpeljave izrekov nikoli ne pripeljejo do protislovij. Leta 1931 je komaj 25-letni avstrijski matematik Kurt Gödel osupnil matematično stroko z dokazom, ki je zamajal temelje matematike. Dokazal je, da bodo v vsakem aksiomatskem sistemu obstajale resnične trditve, ki jih ne bo možno dokazati. Če bi jih vključili kot aksiom, bomo pridelali nove trditve, spet resnične, ki bodo nedokazljive.

To velja ponoviti še enkrat. Pred Gödlom je veljalo, da lahko vsako pravilno trditev dokažemo iz osnovnih aksiomov. Morda tega ne znamo, ker nismo dovolj pametni, morda je dokaz dolg in nič kaj eleganten, a obstaja. Gödel je neizpodbitno v splošnem dokazal, da obstajajo trditve, ki so zagotovo resnične, pa jih ni možno dokazati.

To pomeni, da ne obstaja neodvisna matematična resničnost, v kateri bi domovala teorija vsega. Pred Gödlom je veljalo le, da je od nabora aksiomov odvisno, kaj drži, sedaj pa tudi, kaj je dokazljivo. Njegov izrek o nepopolnosti pravi, da je vsak neprotisloven (konsistenten) nabor aksiomov nujno nepopoln. Iz tega sledi tudi, da noben nabor aksiomov ne more dokazati lastne neprotislovnosti.

Posledice za matematiko so hude. Matematika je polna trditev ali problemov, za katere se predvideva, da držijo, a nam jih še ni uspelo dokazati. S številnimi so se matematiki borili leta in leta. Britanski matematik Andrew Wiles je šele leta 1994 dokazal Fermatov zadnji izrek (celoštevilska rešitev an + bn = cn ne obstaja za n > 2), ki ga je ta predpostavil leta 1637. Vmes je poskusilo veliko drugih, a jim je spodletelo. Toda po Gödlu za težke matematične probleme ne moremo biti prepričani, ali morda niso zgolj nerešljivi.

Da posledice segajo tudi v fiziko, je britanski matematik Alan Turing pokazal že leta 1936. Turinga poznamo predvsem po konceptu idealnega računalnika, ki izvaja ukaze in se imenuje Turingov stroj, s čimer je definiral mehanski program kot algoritem. Še danes so računalniki matematično ekvivalentni Turingovim strojem. Turing je iz Gödlovega izreka izpeljal, da obstajajo algoritmi (računalniški programi), za katere ni možno določiti, ali se bodo izvajali neskončno časa ali pa se bodo končali.

Samotne poti na platonskih telesih

Platonska telesa so najpravilnejša med oglatimi telesi: gradijo jih sami enaki pravilni mnogokotniki (trikotniki, kvadrati ali petkotniki), tako da se v vsakem oglišču stika enako število teh mnogokotnikov. O teh telesih so razmišljali številni starogrški matematiki, rigorozno pa jih je opisal Evklid. Pokazal je, da v treh dimenzijah obstaja pet platonskih teles: tetraeder, kocka, oktaeder, ikozaeder in dodekaeder. In tudi dva tisoč let kasneje šele spoznavamo nekatere njihove lastnosti, kar je za tako preprosta telesa pravzaprav neverjetno.

Zamislimo si, da stojimo na oglišču enega izmed teh teles. Ali obstaja ravna pot po telesu, ki bi nas pripeljala nazaj na isto izhodišče, ne da bi šla skozi katerokoli drugo oglišče? Z drugimi besedami: ali obstaja geodetka, ki poteka skozi eno samo oglišče. S tem vprašanjem so si matematiki belili glavo stoletja, potem pa so pred štirimi leti ugotovili, da za tetraeder, kocko, oktaeder in ikozaeder takih poti ni. Kamorkoli se iz enega oglišča odpravimo, bomo najprej zadeli kakšno drugo oglišče ali pa nikoli nobenega oglišča več.

Pričakovali bi, da je za dodekaeder odgovor enak, a dokaza ni bilo. Jayadev Athreya z univerze v Seattlu ter David Aulicino in Patrick Hooper z newyorške univerze pa so avgusta letos pokazali, da je presenetljiv odgovor da. Ne le da obstaja ena taka pot, obstaja jih neskončno mnogo, ki jih lahko razvrstijo v 31 skupin. Bistvena razlika med četverico in dodekaedrom so mnogokotniki. S kvadrati (kocka) oziroma trikotniki (tetraeder, oktaeder, ikozaeder) je možno tlakovati celotno ravnino, s petkotniki (dodekaeder) pa ne. To ima zapletene posledice, med njimi tudi obstoj neskončno mnogo geodetk na dodekaedru, ki potekajo skozi eno samo oglišče.

Anton Zorich s pariškega inštituta za matematiko je pojasnil, da takšnega dokaza ne bi mogli izvesti pred desetimi leti, saj bi potrebovali ogromno programiranja. Athreya, Aulicino in Hooper so si pri dokazu pomagali z računalniškim programom, s katerim so prečesali več možnosti. Niso našli le ene rešitve, temveč vse – problema niso samo rešili, ampak so ga dojeli.

Računalniki na pomoč

Prvič so matematiki neki pomemben izrek dokazali z računalnikom leta 1976, ko sta Kenneth Appel in Wolfgang Haken dokazala izrek o štirih barvah (vsak zemljevid je možno pobarvati že s štirimi barvami, da ne bosta nobeni sosednji državi enake barve). Po prvotni skepsi danes matematiki računalniške dokaze priznavajo, čeprav je strogo gledano v tem primeru v dokazu luknja. Če naj dokaz velja, morajo biti vse predpostavke resnične in vsi koraki preverljivi. Pri računalniških dokazih to ni tako enostavno, je prvi trdil že ameriški filozof Thomas Tymoczko leta 1979.

Deloma mu lahko pritrdimo: takšen dokaz terja implicitno zaupanje v programsko kodo, v prevajalnik v strojno kodo in v izvedbo na ravni strojne opreme. Vseh teh sestavin ne moremo enostavno preveriti, zato se v takšnem primeru zadovoljimo s temeljito preveritvijo in dokazom pravilnosti izvorne kode, ki jo potem izvedemo večkrat, po možnosti na različnih računalniških arhitekturah. Čeprav je s tem letvica rigoroznosti dokaza nekoliko nižja, dandanes takšne dokaze sprejemamo. Navsezadnje računalnikom zaupamo tudi, ko krmilijo letala ali naprave za zunajtelesni krvni obtok.

Včasih matematiki dejansko prečešejo te gore podatkov. Keplerjevo domnevo o najučinkovitejšem zlaganju krogel so leta 1998 dokazali z računalniškim programom, potem pa je 12 matematikov leta kopalo po treh gigabajtih rezultatov, da so dokaz z visoko verjetnostjo razglasili za pravilen.

Kadar računalnike uporabimo za preveritev velikega števila primerov, so v resnici zgolj orodje pri dokazovanju, nekakšni zmogljivi kalkulatorji. Lahko računalnik iz aksiomov ustvari celoten dokaz nekega izreka? Matematik Paul Cohen, ki je prejel tudi Fieldsovo medaljo (najvišje odlikovanje v matematiki, ker Nobelovih nagrad ni), je že v 70. letih zlovešče napovedal, da v prihodnosti matematiki ne bodo več potrebni. Nadomestili jih bodo računalniki.

Danes še nismo tam, a že obstajata dve vrsti pomočnikov. Avtomatizirani dokazovalniki izrekov ( automated theorem prover) uporabljajo surovo računsko moč, da se prebijejo skozi obsežne izračune. Rezultat je preprost odgovor da ali ne in nepregledna množica podatkov, ki je ljudje ne morejo preveriti. Interaktivni dokazovalniki izrekov ( interactive theorem prover) pa so neke vrste pomočniki, ki preverjajo argumente in obstoječe korake ter dejansko pišejo ljudem razumljive dokaze. Obema še precej manjka do popolne avtonomnosti.

Josef Urban s praškega inštituta za informatiko, robotiko in kibernetiko raziskuje ta problem. Julija je njegova skupina objavila skupino domnev skupaj z matematičnimi dokazi, kjer je tako domneve postavil kot dokaze izvedel – računalnik. Christian Szegedy iz Google Researcha, ki se ukvarja s strojnim razumevanjem človeškega jezika, meni, da takšna avtomatizacija prinaša nove globine strojnega razumevanja. Matematik Michael Harris z univerze Columbia ob tem poudarja, da vsa ta orodja od matematikov terjajo učenje pisanja računalniške kode, medtem ko bi se lahko ukvarjali z matematiko. Prepričan je, da računalniki ne bodo nikoli zamenjali matematikov. S tem se strinja tudi Kevin Buzzard z londonskega Imperial Collegea, ki pojasnjuje, da računalniki niso sami rešili še nobenega res težkega problema. Dokler ne bodo prvega, bo matematike težko prepričati, da so zamenljivi.

Tudi če računalniki ne bodo nikoli zamenjali matematikov, njihovega prispevka ne bo mogoče prezreti. Pomembno vlogo imajo pri izobraževanju, saj že danes obstajajo pripomočki, ki prikazujejo reševanje šolskih problemov po korakih (na primer odvajanja). Računalniški dokazi so še korak dlje za poučevanje. Konec koncev pa so računalniki uporabni tudi pri preverjanju. Ruski matematik Vladimir Aleksandrovič Vojevodski je že leta 1999 v enem svojih dokazov pri preverjanju z računalnikom našel napako. Morda bodo v prihodnosti računalniki prevzeli del nalog recenzentov v znanstvenih revijah, sklene Timothy Gowers s Cambridgea.

Dr. Matej Huš je znanstveni sodelavec na Kemijskem inštitutu, kjer raziskuje kemijske procese na ravni kvantne mehanike.

• Stari Grki so prvi sistematično definirali sistem aksiomov in izpeljevanja izrekov v matematiki.

• Evklidovi Elementi so na Zahodu za Svetim pismom druga najbolj citirana knjiga.

• Prvi pomemben izrek, ki so ga matematiki dokazali z računalnikom, je leta 1976 dokazan izrek o štirih barvah.

Kurt Gödel je zamajal temelje matematike, ko je dokazal, da bodo v vsakem aksiomatskem sistemu obstajale resnične trditve, ki jih ne bo možno dokazati. To pomeni, da ne obstaja neodvisna matematična resničnost, v kateri bi domovala teorija vsega.