London learns Lean
3 PM, 28 Mar 2025
Mathematicians across London share their work on the formalisation of mathematics using the AI proof-assistant computer language Lean.
In a session co-chaired by Prof. Kevin Buzzard of Imperial College London and Prof. Richard Hill of University College London, researchers and PhD students discuss their projects in the area of formal proof verification in Lean. The meeting includes visitors from Imperial, UCL, the University of Cambridge and Google DeepMind as well as the London Institute, fostering collaboration across a wide swathe of mathematics.




LCP











