Peter LeFanu Lumsdaine, Anders Mörtberg: PhD course: Computer Formalisation of Mathematics
Tid: Må 2025-01-27 kl 15.30
Plats: Cramérrummet
Medverkande: Peter LeFanu Lumsdaine, Anders Mörtberg
The course will give a thorough practical introduction to formalising mathematics in programs like Lean (primarily), Rocq/Coq, and Agda, along with some more theoretical work on the formal logical systems underlying these programs. The course aims to be broadly accessible, assuming just a general mathematics background — no prior logic or programming experience required.