Mini Course – Lean proof assistant workshop Mr. Antoine de Saint Germain (Department of Mathematics, HKU) [LINK]