Seminar series
Date
Mon, 05 May 2025
14:15
14:15
Location
L5
Speaker
Heather Macbeth
Organisation
Imperial College London
The last ten years have seen extensive experimentation with computer formalisation systems such as Lean. It is now clear that these systems can express arbitrarily abstract mathematical definitions, and arbitrarily complicated mathematical proofs.
The current situation, then, is that everything is possible in principle -- and comparatively little is possible yet in practice! In this talk I will survey the state of the art in geometry (differential and algebraic). I will outline the current frontier of what has been formalised, and I will try to explain the main obstacles to progress.