i i \Mohoric" | 2022/9/19 | 8:27 | page 124 | #3 i i i i i i Vesti ukrivljenosti na tvorbo in zbiranje topolo skih defektov v tankih nemati c- nih plasteh, (ii) mehanizem »zunanje ukrivljenosti«, ki razlo zi anomalno siroko podro cje geometrijske stabilnosti celic rde cih krvni ck v sesalcih, in (iii) mehanizem ADCT (adaptivedefect-core-targeting), ki napoveduje, pod kak snimi pogoji defekti u cinkovito zajemajo nanodelce. (iv) Razvil je tudi prvi teoreti cni model elektrokalori cnega pojava v nemati cnih in smekti c- nih A teko cih kristalih, na podlagi katerega so odkrili anomalno ob cutljiv re zim. V slednjem so eksperimentalno izmerili rekordno vrednost elektro- kalori cnega odziva v teko cih kristalih, ki je dovolj velik, da lahko vodi do razvoja hladilnih in grelnih sistemov nove generacije. Vsem nagrajencem iskreno cestitamo za uspeh in priznanje. LITERATURA [1] https://www.gov.si/novice/2020-12-01-znane-so-letosnje-prejemnice-in-prejemniki- nagrad-in-priznanj-za-izjemne-dosezke-v-znanstveno-raziskovalni-dejavnosti/, dostop 8. 10. 2020. Ale s Mohori c Andrej Bauer prejemnik nagrade Levija L. Conanta 2022 Prof. dr. Andrej Bauer, profesor ra cunalni ske matematike na Fakulteti za matematiko in ziko Univerze v Ljubljani, je od American Mathematical Society prejel nagrado Levija L. Conanta za leto 2022 za clanek z naslovom Five stages of accepting constructive mathematics (Pet faz sprejemanja kon- struktivne matematike) [1]. V spomin na Levija L. Conanta, matematika in pedagoga, ki je bil znan po svojem odli cnem pedago skem delu, se nagrada podeljuje od leta 2000 za najbolj si ekspozicijski clanek, objavljen v revijah Bulletin of the American Mathematical Society in Notices of the American Mathematical Society v preteklih petih letih. Novica je objavljena na spletni strani AMS na povezavi https://www.ams.org/news?news_id=6827. Bauer se je rodil leta 1971 v Ljubljani. Diplomiral je leta 1994 pod men- torstvom prof. dr. Du sana Repov sa na Fakulteti za matematiko in ziko Univerze v Ljubljani na programu matematika, teoreti cna smer. Za di- plomsko delo z naslovom Seifertovi vlaknati prostori je prejel univerzitetno Pre sernovo nagrado. Na pobudo prof. dr. Marka Petkov ska se je odpravil na doktorski studij na Carnegie Mellon University v ZDA, kjer je leta 2000 dok- toriral pod mentorstvom prof. dr. Danea Scotta. Oddelek za ra cunalni stvo univerze Carnegie Mellon je Bauerju za doktorsko disertacijo z naslovom The Realizability Approach to Computable Analysis and Topology podelil studentsko nagrado. S konstruktivno matematiko se je sre ceval ze v casu 124 Obzornik mat. fiz.69 (2022) 3 i i \Mohoric" | 2022/9/19 | 8:27 | page 125 | #4 i i i i i i Andrej Bauer prejemnik nagrade Levija L. Conanta 2022 doktorskega studija, saj je tesno povezana s teorijo izra cunljivosti, ki jo je Bauer uporabil na konstrukcijah iz analize in topologije. Po kon canem dok- toratu je Bauer leto pre zivel na in stitutu Mittag-Leer na Svedskem, kjer je v okviru posebnega raziskovalnega programa za logiko nadaljeval raziskave. Pot ga je vodila nazaj v Ljubljano, kjer se je na Fakulteti za matematiko in ziko Univerze v Ljubljani zaposlil kot visoko solski u citelj in leta 2014 postal redni univerzitetni profesor. Med letoma 2012 in 2013 je na in stitutu Institute for Advanced Study (IAS) v Princetonu, ZDA, potekalo posebno leto, namenjeno univalentnim temeljem matematike. Bauer se je pridru zil vodilnim znanstvenikom na podro cju teorij tipov in dokazovalnih pomo cnikov. Skupaj so razvili novo osnovo matematike, homotopsko teorijo tipov (HoTT), ki temelji na idejah konstruktivne matematike in zdru zuje teorijo tipov s principi homotopske teorije. Kot produkt plodovitega leta je iz sla knjiga Homotopy Type The- ory [2], ki je postala osnova za studijo HoTT. Kasneje je homotopska teorija tipov do zivela tudi implementacijo kot knji znica dokazovalnega pomo cnika Coq, imenovana HoTT Library [5], katere za cetnik je bil prav Bauer. Knji- znico so razvijali stevilni strokovnjaki, skupnost uporabnikov in razvijalcev pa se se vedno siri. Raziskovalno se Bauer poleg studije homotopske teorije tipov ukvarja tudi s sinteti cno izra cunljivostjo ter algebrajskimi u cinki in njihovimi pre- strezniki, ki sta jih utemeljila [6] skupaj z doc. dr. Matijo Pretnarjem. Dan- dana snji se Bauer posve ca raziskovanju metateorije teorij tipov, razvoju dokazovalnega pomo cnika Andromeda ter formalizaciji posameznih podro- cij diskretne matematike z dokazovalnim pomo cnikom Lean. Bil je mentor stevilnim dodiplomskim in magistrskim studentom, na doktorskem studiju pa je vodil dr. Davorina Le snika, ddr. Melito Hajdinjak, dr. Philippa Georga Haselwarterja, dr. Anjo Petkovi c Komel in Jureta Taslaka. Na Fakulteti za matematiko in ziko Univerze v Ljubljani Bauer vodi raziskovalni seminar za temelje matematike in teoreti cno ra cunalni stvo. Bauer je zelo dejaven tudi kot clan sir se matemati cne skupnosti na spletu. V svojem blogu z naslovom Mathematics and Computation objavlja misli, ki so morda prekratke za clanek, ali pa clanke, predstavitve, videe in zapise pospremi z dodatno intuitivno razlago, da tako la zje dose zejo bralca. Na forumu StackExchange je ob casu pisanja tega prispevka v kategoriji ra- cunalni stva (Computer science) med 20 najbolj aktivnimi clani, v kategoriji teoreti cnega ra cunalni stva (Theoretical computer science) pa je celo najbolj aktiven clan s stevilnimi prispevki in odgovori na vpra sanja. Na forumih aktivno prispeva tudi na podro cju matematike (Mathematics, MathOver- ow), nedavno pa je povezal raziskovalce in ustanovil forum za dokazovalne Obzornik mat. fiz.69 (2022) 3 125 i i \Mohoric" | 2022/9/19 | 8:27 | page 126 | #5 i i i i i i Vesti pomo cnike (Proof assistants). Znanstvene ideje siri tudi v medijih, v po- govornih oddajah (na primer Nedeljski gost na Valu 202), informativnih oddajah in drugod. Na IAS so v letu namenjenem raziskovanju temeljev matematike pote- kali tudi seminarji za sir so matemati cno publiko, kjer je Bauer hudomu sno predstavil ideje konstruktivne matematike [4] preko petih faz zalovanja, kot jih je opisala Elisabeth Kubler-Ross v svoji knjigi On Death and Dying [3]: zanikanje, jeza, pogajanje, depresija in sprejemanje. Med slu satelji je bil tudi prof. dr. Mark Goresky, urednik revije Bulletin of the American Ma- thematical Society, ki je Bauerja spodbudil in podpiral, da je predavanje nadgradil v (nagrajeni) clanek [1]. Idejo konstruktivne matematike marsikdo prehitro zavrne, ker ima o njej napa cno predstavo. Zato v clanku Bauer bralcu najprej v fazi zanikanja po- jasni, kaj konstruktivna matematika pravzaprav je: to je matematika, ki ne uporablja zakona o izklju cenem tretjem , ki pravi, da za vsako izjavno spremenljivko P velja P _:P . To seveda ne pomeni, da konstruktivizem dopu s ca neko »tretjo« mo znost, saj tudi v konstruktivni matematiki ve- lja zakon o neprotislovju, ki trdi, da ne obstaja izjava P , za katero velja P ^:P . Faza zanikanja se nadaljuje z razlikovanjem med dokazom ne- gacije, ki je kot logi cni sklep prisoten tudi v konstruktivni matematiki, in dokazom s protislovjem, ki pa je ekvivalenten zakonu o izklju cenem tretjem in ga konstruktivna matematika ne zajema. Na primerih Russelovega pa- radoksa in dokaza obstoja iracionalnih stevil a in b, katerih potenca a b je racionalna, Bauer ilustrira, da za mnoge matemati cne izreke lahko najdemo povsem intuitivne konstruktivne dokaze. V zadnjem delu faze zanikanja se Bauer posveti aksiomu izbire in poda dokaz, da iz aksioma izbire sledi za- kon o izklju cenem tretjem, ter na primeru Lebesgueovega izreka o pokritju znova poka ze, da se je pogosto mogo ce izogniti nepotrebni uporabi aksioma izbire v prid konstruktivnemu dokazu. Sledi kratka faza jeze, kjer se Bauer dotakne nekaj zgodovinskih vzgibov in odzivov na konstruktivno matematiko. Se posebej provocira z izrekom, da je zakon o izklju cenem tretjem ekvivalenten izjavi, da so podmno zice kon cne mno zice kon cne, kar primerja z nekaterimi drugimi drznimi matemati cnimi konstrukcijami (neevklidske geometrije, Weirstrassova nikjer odvedljiva zve- zna funkcija, izrek Banach-Tarskega), ki so prav tako v preteklosti dvigovale prah, pa smo s casoma sprejeli njihove matemati cne razlage. V fazi pogajanja Bauer bralcu, ki je tipi cno vzgojen v duhu klasi cne ma- tematike, pojasni, kako se sploh lotiti konstruktivne matematike. Za la zjo inuticijo mu predstavi nekaj modelov konstruktivne matematike. Posebno pozornost posveti realizabilnosti, povsem konstruktivnemu modelu, kjer je 126 Obzornik mat. fiz.69 (2022) 3 i i \Mohoric" | 2022/9/19 | 8:27 | page 127 | #6 i i i i i i Andrej Bauer prejemnik nagrade Levija L. Conanta 2022 resni cno le tisto, kar je mogo ce izra cunati. Program, ki slu zi kot pri ca re- sni cnosti izjave, se imenuje realizator. Bauer doka ze, da zakon o izklju cenem tretjem nima realizatorja in zato ne velja v modelu realizabilnosti. Nadalje Bauer predstavi topos sve znjev na topolo skem prostoru X kot model kon- struktivne matematike, kjer so resni cnostne vrednosti odprte podmno zice X. Zakon o izklju cenem tretjem je v tem modelu ekvivalenten dejstvu, da odprte in zaprte mno zice sovpadajo, cemur zado s cajo zgolj zelo speci cni topolo ski prostori X. S pomo cjo Arhimedovega aksioma, da za vsako realno stevilo x obstaja strogo ve cje celo stevilo k, Bauer pojasni, zakaj v modelu aksiom izbire ne velja. Nato nas Bauer popelje na kratek panoramski pregled mnogih konstruk- tivnih modelov matematike, od Grothendieckovih toposov do homotopske teorije tipov. Ker se izka ze, da je konstruktivnih vesolij neznosno mnogo, Bauer to popotovanje saljivo poimenuje faza depresije, in se hkrati poigra s primerjavo, da so se matematiki tudi znotraj teorije mno zic sre cali z mno- gimi svetovi klasi cne matematike. V zaklju cni fazi sprejemanja Bauer poka ze, kako konstruktivisti cna per- spektiva spreminja pogled na matemati cne denicije, dokaze in izreke. Na zgledu izreka o srednji vrednosti in izreka Tihonova nam ilustrira, kako ma- temati cne pojme reformuliramo v klasi cno ekvivalentne in konstruktivno veljavne razli cice. Konstruktivizem nam tako odstira nov bogatej si pogled na matemati cne konstrukcije. Za prejeto nagrado Andreju Bauerju iskreno cestitamo in mu zelimo veliko navdiha in uspeha pri nadaljnjem delu! LITERATURA [1] A. Bauer, Five stages of accepting constructive mathematics, Bull. Amer. Math. Soc. (N. S.) 54 (2017), 481{498. [2] The Univalent Foundations Program, Homotopy Type Theory: Univalent Fo- undations of Mathematics, Institute for Advanced Study, 2013, dostopno na homotopytypetheory.org/book, ogled 3. marca 2022. [3] E. Kubler-Ross, On Death and Dying, New York, Routledge, 1969. [4] A. Bauer, Five stages of accepting consturctive mathematics, Predavanje na School of Mathematics, Institute for Advanced Study, Princeton, ZDA, 2013, dostopno na www.youtube.com/watch?v=21qPOReu4FI, ogled 3. marca 2022. [5] A. Bauer, J. Gross, P. LeFanu Lumsdaine, M. Shulman, M. Sozeau in B. Spitters, The HoTT Library: A formalization of homotopy type theory in Coq, 2016. [6] A. Bauer in M. Pretnar, Programming with algebraic eects and handlers , J. Log. Algebr. Methods Program., Elsevier BV 84 (2015), 108{123. Anja Petkovi c Komel Obzornik mat. fiz.69 (2022) 3 127