A Crash Course About Formalizing Mathematics In Lean-3
The aim of this series of lectures is to give a brief introduction to formalization of mathematics in LEAN-3 , a proof assistant which has recently proven to be particular well-suited for encoding modern mathematics.