Gagnvirkar tölvusannanir

Fyrsti fyrirlestur ársins 2023 á vegum ÍSF verður haldinn fimmtudaginn 9. febrúar kl. 17. Fyrirlesari er Dagur Tómas Ásgeirsson. Dagur stundar doktorsnám við Hafnarháskóla.

Ágrip: Forritunarmálið Lean er gagnvirkur sannari (e. interactive theorem prover), sem kann núorðið mestalla stærðfræði sem er kennd í BS-námi, og meira til. Útskýrt verður hvað þetta þýðir, og fjallað um það hvernig stærðfræðingar gætu í náinni framtíð notað Lean eða önnur svipuð tól sér til aðstoðar við rannsóknastörf. Ennfremur verður útskýrt með sýnidæmum hvernig hægt er að nota gagnvirka sannara sem hjálpartæki í stærðfræðikennslu.