PPS-Lean: A Formalisation Project This project aims to formalise the results taught in the University of Edinburgh's Proofs and Problem Solving course.