In recent years there has been a push (in particular by the Lean community) to formalise the kind of mathematics which is going on right now in mathematics departments. This represents a big change from what was happening a decade ago, where most formalisations of mathematics were either foundational (e.g. experiments in type theory), elementary (e.g. undergraduate level) or were rigorously checking computer-assisted proofs. I’ll give an overview of the landscape and how it has changed, why it’s changed, where it’s going and why it’s going there. Note: I will not assume a heavy mathematical background; the talk is absolutely suitable for computer scientists interested in formalisation.