Pages Menu
Categories Menu

Posted on 17.11.21 in Featured, Univerze, Video

prof. dr. Andrej Bauer, FMF  UL,   prejemnik Conantove nagrade 2022

prof. dr. Andrej Bauer, FMF UL, prejemnik Conantove nagrade 2022

Profesor računalniške matematike na Fakulteti za matmatiko in fiziko (FMF) Univerze v Ljubljani (UL) Andrej Bauer, se ponaša z nagrado AMS Levija L. Conanta za članek »Five stages of accepting constructive mathematics«, Bulletin of the AMS, 54 (2017), 481-498.

Bauerjev članek je uvod v konstruktivno matematiko. S pojasnjevanjem osnovne predpostavke konstruktivne matematike, namreč da opustimo zakon o izključeni tretji možnosti –  hitro potem 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 konstruktivizma. 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.

Slika prikazuje delček homotopske teorije tipov, ki jih je dr. Bauer razvijal v sodelovanju s kolegi na Institute of Advanced Study v Princetonu

Da osvajanje zapletenih znanj nima kraljevske poti, Bauer ponazori z izjavo: „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 urjenje.“

Mnogi matematiki so namreč skeptični ali celo sovražni do 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 zdaj morda niso cenili – celo v povezavi z zadevami, za katere so mislili, da jih že razumejo.

Doseganje tako uglednih nagrad je plod leta dela in  študija in kot je v Bauerjevem primeru, študija zahtevnih področij matematike. Po diplomi na Fakulteti za matematiko in fiziko (FMF) na UL, je doktoriral iz čiste in  aplikativne logike na Carnegie Mellon University pod mentorstvom Dane S. Scotta. Zatem  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 pa se ukvarja s teorijo tipov in načrtovanjem dokazovalnih pomočnikov.

Foto: AB/osebni arhiv

Post a Reply

Your email address will not be published. Required fields are marked *