Formalisation, AI and the role of mathlibMPIM
by
MPIM, Vivatsgasse, 7 - Lecture Hall
Max Planck Institute for Mathematics
Mathematics and AI Discussion Seminar
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. Formalisation of mathematics has come of age now: in recent years and months, there has been spectacular progress in formalising research-level mathematics in diverse fields. In fact, recent AI-assisted 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. I will discuss what this means for human formalisation and the mathlib library in particular: despite the rapidly changing ecosystem, they still take an important role, for the ecosystem and human understanding.
More information about the Mathematics and AI seminar can be found on its website:
https://challeckdube.github.io/mathematics-and-ai-seminar.html