SMRI Colloquium: Buzzard -- On the formalisation of mathematics

Thursday 12 November 2026 - Special SMRI Colloquium and Q & A "Formalisation, AI and
mathematics" with Kevin Buzzard, Imperial College London.  

Lunch will be served at SMRI aT 12.00 noon prior to the colloquium and afternoon tea
will be served on the terrace at SMRI at 2.30pm after the Q & A.  

Colloquium on "On the formalisation of mathematics" presented by Kevin Buzzard, Imperial
College London.  Followed by a Q & A on "AI and mathematics" moderated by Oded Yacobi.  

Abstract: Formalisation is the process of translating mathematics from "natural
language" (like English) into a formal language such as Lean.  I will give an
introduction and brief history of the field, followed by an explanation of what has been
going on recently, particularly with regards to autoformalisation (which is when a
computer does the translation), and I'll end with some speculation about the future of
this fast-moving area.  The talk will be for a general mathematical audience, and no
expertise in Lean is necessary.  

Event details: 

12.00-1.00pm Lunch at SMRI 

1.00-2.30 pm SMRI Colloquium and Q&A in the Heydon Laurence Lecture Theatre 217, Heydon
Laurence Building (A08.02.217) Science Road.  

2.30-3.30 Afternoon tea on the terrace at SMRI.