Næsta málstofa verður þriðjudaginn 7. mars kl 13:20 í Naustinu, húsi Endurmenntunar.
Fyrirlesari er Dagur Tómas Ásgeirsson, Kaupmannahafnarháskóla (og Háskóla Íslands).
Titill fyrirlestrarins er Interactive theorem proving.
Ágrip: The programming language Lean is an interactive theorem prover which now comes with a formalised mathematical library that contains most of an undergraduate degree in mathematics, and more. We will give a live demo of formalising mathematics in Lean, as well as discussing several ways in which mathematicians could use this tool, both in research and teaching, in the near future.