Formalisation, AI and the role of mathlibMPIM

by Michael Rothgang (Universität Bonn)

Friday Oct 30, 2026, 3:45 PM → 4:45 PM Europe/Berlin

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