Math and AI · Event Information
Formalisation of mathematics: insight into an ongoing revolution
A talk by Michael Rothgang (Bonn University).
Registration is now closed
Thank you for your interest in this event.
Zoom access details will be sent to registered participants.
Abstract
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.