Peter LeFanu Lumsdaine, Anders Mörtberg: PhD course: Computer Formalisation of Mathematics

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.