Formalisation of mathematics: insight into an ongoing revolution

Digitising or formalising mathematics refers to translating mathematical arguments from natural language (e.g. English) into a computer-readable format: this makes it possible to verify proofs with certainty, often improves mathematical understanding, can transform peer-review and enables new levels of collaboration. In recent years and months, there has been spectacular progress in formalising research-level mathematics in diverse fields. In fact, recent breakthroughs (such as, on the Navier-Stokes equations) have been enabled through formalisation. I will explain what the excitement is about and give an idea of the current state of the art.To illustrate this point, I will explain the state of the art in differential geometry: there is much more to it than prompting an AI. Already finding the correct general definition is a non-trivial mathematical question. I will survey what is currently formalised, what is being worked on and where you can help. I will also comment on technical challenges of working with manifolds in Lean and how to address them.