- see Imperial College course-work - See existing LEAN texts - Examine value of LEAN-based courses in proof validity - Extend LEAN to applied mathematics: - Differential equations - Engineering evaluation of order of magnitude errors -