A formalisation of Natural Deduction in Lean and associated Models, from the 2nd Year subject Logical Methods.