Prof. dr. Andrej Bauer (foto: Marko Cokan - Foto Kozama)
Datum objave: 28.10.2021
Kategorija: Raziskovalci v objektivu, Naš prispevek k ciljem trajnostnega razvoja OZN
Cilji trajnostnega razvoja: 4 Kakovostno izobraževanje (kazalniki)
Prof. dr. Andrej Bauer, profesor računalniške matematike na Fakulteti za matematiko in fiziko Univerze v Ljubljani, bo v letu 2022 prejemnik prestižne nagrade Ameriškega matematičnega združenja (AMS - American Mathematical Society) Levija L. Conanta za članek »Pet korakov v sprejemanju konstruktivne matematike«. Nagrada Levija L. Conanta je priznanje za najboljši ekspozicijski članek, objavljen v zadnjih petih letih v Notices of the AMS ali Bulletin of the American Mathematical Society. Nagrada za leto 2022 bo podeljena 5. januarja 2022 na Joint Mathematics Meetings 2022 v Seattlu.
Bauerjev članek je uvod v konstruktivno matematiko. Ta se od klasične razlikuje v opustitvi Aristotelovega zakona o izključeni tretji možnosti in je na področju matematičnih ved dolgo veljala za obrobno področje, s katerim se je ukvarjalo relativno majhno število matematikov. V zadnjem času pa je konstruktivna matematika našla svoje sidrišče v računalništvu, saj ima pomembno lastnost: vsak dokaz, račun ali konstrukcijo, ki jo izvedemo v sklopu konstruktivne matematike, lahko sistematično prevedemo v računalniški program. (Na primer, konstruktivni dokaz o obstoju rešitve diferencialne enačbe nam hkrati omogoča tudi računanje rešitev enačbe z računalnikom.) Matematiki in računalničarji so v zadnjih desetletjih razvili računalniška orodja, zasnovana na tej ideji. Z njimi lahko sestavljamo programe, katerih pravilnost je formalno preverjena z računalnikom.
Kot so zapisali pri AMS, Bauer v svojem članku najprej poda osnovno predpostavko konstruktivne matematike in ta je, da opustimo zakon o izključeni tretji možnosti – nato pa hitro razreši nekaj pogostih napak v njenem razumevanju. Pojasni Diaconescoujev rezultat, da iz aksioma izbire sledi izključena tretja možnost, nato pa dokaže, da je le-ta ekvivalentna izjavi, da so vse podmnožice končne množice (v konstruktivnem smislu) končne. Članek zlagoma predstavi nekaj osnovnih idej matematičnega konstruktivizma. V nadaljevanju Bauer bralca vodi skozi prve, otroške korake konstruktivne matematike, kjer že majhne variacije v formulaciji izrekov (sicer nezaznavne z nekonstruktivnega stališča) povzročijo velike spremembe.
Mnogi matematiki so skeptični ali celo sovražni do matematičnega konstruktivizma. Bauerjev članek neposredno nagovarja take bralce in jih popelje na voden ogled skozi vrtove konstruktivne matematike. Čeprav je malo verjetno, da bo po prebiranju članka večina matematikov spremenila svoj osnovni način matematičnega delovanja, je zelo malo takih, ki jim članek ne bi predočil načina razmišljanja, ki ga do sedaj morda niso cenili – celo v povezavi z zadevami, za katere so mislili, da jih že razumejo. Vse to je opravljeno s pronicljivim humorjem in potrpežljivostjo. To je članek, čigar ideje bodo ostale z bralcem še dolgo po tem, ko ga je prebral.
Ob prejetju nagrade je Andrej Bauer povedal:
»Resnično sem počaščen in hvaležen za nagrado Levija L. Conanta v 2022. Zahvaljejem se AMS, da je prepoznala trud, ki je bil vložen v članek, ter uredniku Marku Goreskyemu za prijazno in vztrajno spodbudo, ki me je vodila, dokler članek ni prevzel sprejemljive oblike. To je tudi dobra priložnost, da izrazim hvaležnost majhni, a trdoživi skupnosti konstruktivne matematike, ki mi je dala veliko več, kot ji bom lahko kadarkoli povrnil.
S konstruktivno matematiko sem se prvič srečal med podiplomskim študijem, ko sem proučeval izračunljivost v analizi in topologiji. Še vedno se spomnim, kako težko se je bilo naučiti konstruktivnega razmišljanja in zatreti instinkte, ki jih je vgradilo klasično matematično urejenje. Ko sem postal učitelj, sem z veseljem razlagal konstruktivno matematiko študentom, kolegom in neznancem na medmrežju. Sčasoma je postajala moja pomoč pri prestopanju običajnih kamnov spotike in odpravljanju napačnih predstav, ki so ovirale intuicijo, vse boljša. Članek »Five stages of accepting constructive mathematics« je skupek vseh teh izkušenj, pa tudi iskreno razkritje mojih osebnih pogledov na konstruktivno matematiko in matematiko nasploh.«
Biografska skica Andreja Bauerja
Andrej Bauer je profesor računalniške matematike na Fakulteti za matematiko in fiziko Univerze v Ljubljani. Leta 1994 je diplomiral na področju matematike na Univerzi v Ljubljani, nato pa leta 2000 prejel doktorat iz čiste in aplikativne logike na Carnegie Mellon University pod mentorstvom Dane S. Scotta. Leta 2001 je preživel semester na Mittag-Leffler Institute v Stockholmu na Švedskem. Leta 2012 je bil član Institute for Advanced Study, kjer je sodeloval pri razvoju homotopske teorije tipov. Bauerjevo delo zajema temelje matematike, konstruktivno in izračunljivo matematiko, teorijo tipov, homotopsko teorijo tipov ter matematične principe programskih jezikov. Je soavtor knjige »Homotopy Type Theory: Univalent Foundations of Mathematics« in pobudnik knjižnice HoTT, ki je obsežna formalizacija homotopske teorije tipov v dokazovalnem pomočniku Coq. Znan je tudi po ključnih prispevkih na področju programiranja z algebraičnimi učinki in prestrezniki. V zadnjem času se ukvarja s teorijo tipov in načrtovanjem dokazovalnih pomočnikov.
Bauer posveča pozornost tudi predstavitvam matematike širši javnosti, izven področja matematike pa se ukvarja z računalniško generirano umetnostjo in aikidom, v katerem ima mojstrski naziv. Prijazno vas vabimo tudi k ogledu Bauerjevega predavanja “Five Stages of Accepting Constructive Mathematics” na Institute for Advanced Study, ki je bilo izhodišče nagrajenega članka.
*Besedilo je v večji meri povzeto po besedilu objavljenem na strani AMS: https://www.ams.org/news?news_id=6827
Algebraična števila (avtor: Andrej Bauer)
Algebraična števila so kompleksna števila, ki so koreni polinomskih enačb s celoštevilskimi koeficienti. Slika prikazuje algebraična števila, ki so koreni polinomov stopnje do 5. Barva predstavlja stopnjo polinoma in polmer velikost njegovih koeficientov. Na sliki je skupno 10469668 algebraičnih števil. Slika je bila razstavljena na razstavi, ki jo je Fakulteta za matematiko in fiziko leta 2019 pripravila ob 100-obletnici Univerze v Ljubljani v Jakopičevem drevoredu v parku Tivoli.