Till innehåll på sidan

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

Exportera till kalender

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.