Z Anjo Petković o dokazovalnih pomočnikih v matematiki. #MetaPHoDcast Anja Petković je doktorska študentka na Fakulteti za matematiko in fiziko. Poznate jo lahko tudi iz oddaje Ugriznimo znanost, kjer gledalkam in gledalcem zastavlja matematične uganke. Anja je del raziskovalne ekipe, ki razvija dokazovalne pomočnike. Matematiki in matematičarke v svojem delu oblikujejo izreke. Da preverijo, ali neki izrek ali trditev zares drži, konstruirajo dokaze. A še vseeno je potrebno preveriti, da se matematiki in matematičarke pri dokazih ne zmotijo. Kljub temu, da obstaja rigorozen sistem strokovnega preverjanja dokazov v znanstvenih objavah z recenzijskim postopkom (peer review), se lahko napake izmuznejo tudi v recenziji. Kot pove Anja, se je to kar nekajkrat v matematiki že zgodilo. Zato je morda bolje, da dokazov ne preverjajo ljudje, ampak sklepe matematikov in matematičark preveri računalnik. To je vodilo v pospešen razvoj dokazovalnih pomočnikov, torej računalniških programov, ki nam pomagajo preverjati sklepe v dokazih. Enega takšnih dokazovalnih pomočnikov razvijajo tudi v raziskovalni skupini, v kateri sodeluje Anja, imenuje se Andromeda. Ta je poseben v tem, da lahko uporabnik ali uporabnica sam določi, katero teorijo tipov želi uporabljati. Izkaže se namreč, da je nekatere izreke lažje dokazati v eni teoriji, druge pa v kakšni drugi teoriji tipov. Anja se ukvarja s tem, kako bi v splošnem podali prevedbe (transformacije) med teorijami tipov, da bi lahko združevali dokaze v različnih teorijah. Med pripravo doktorata je spoznala, zakaj študij na doktorski ravni traja vsaj tri leta, in ta tri, štiri leta študija bi z veseljem še enkrat ponovila. Predsedniku vlade bi predlagala, da znanstvenice in znanstveniki dobijo čim boljše pogoje dela. Poklic raziskovalke ali raziskovalca je lahko zelo omejujoč, saj vključuje veliko pogodb za določen čas. Tako se mladi veliko selijo s podoktorskega izobraževanja na podoktorsko izobraževanje znotraj države in tudi krožijo med različnimi državami. Anja predlaga tudi večji vložek denarja v znanost, saj se z znanostjo rešujejo tudi problemi, s katerimi se soočamo kot družba, kot so npr. podnebne spremembe. Želi si tudi, da so razpisi usklajeni z zakonodajo in da je zakonodaja takšna, da je prijazna do znanstvenic in znanstvenikov. Tukaj Anja opozori predvsem na razpisne pogoje v primerih porodniškega dopusta in dopusta za varstvo in nego otroka. Anja pri svojem delu uporablja programsko orodje LaTeX in znotraj njega predlaga uporabo paketa BibTeX za nabor in navajanje izbrane literature. V ogled priporoča Ugriznimo znanost. V branje predlaga knjige Sapiens: Kratka zgodovina človeštva, Homo deus: Kratka zgodovina prihodnosti in 21. nasvetov za 21. stoletje avtorja Yuvala Noaha Hararija; Bad Blood: Secrets and Lies in a Silicon Valley Startup, avtorja Johna Carreyroua; Rojstvo teorema, avtorja Cedrica Villanija; Stric Petros in Goldbachova domena (Uncle Petros and Goldbach’s Conjecture), avtorja Apostolos Doxiadisa. Programerkam in programerjem priporoča ogled spletne strani Project Euler.