Kevin Buzzard - Mathematical Foundations of AI Conference 2026

Kevin Buzzard | On Autoformalization Can artificial intelligence learn to translate mathematical proofs into a language that computers can verify? Kevin Buzzard, Professor of Pure Mathematics at Imperial College London, examines autoformalization: the use of artificial intelligence to translate mathematics written in ordinary human language into formal mathematical systems such as Lean. A leading advocate of computer-assisted proof verification, Buzzard is involved in efforts to formalise some of mathematics' most important results, including Fermat's Last Theorem. His talk explores recent advances in AI-assisted formalization and considers how these technologies might change the way mathematicians develop, communicate and verify proofs. This talk was recorded at the Mathematical Foundations of AI Conference 2026, organised by the Erlangen AI Hub at the University of Oxford, 1–3 September 2026. Find out more: https://erlangenhub.ox.ac.uk/ #ArtificialIntelligence #Mathematics #FormalVerification #ErlangenAIHub