Verification, Formalisation and Canonisation: Formal Theorem Proving in the Age of AI
Tata Institute for Fundamental Research · Mumbai, India · 6 August 2026
Link to website
Interactive Theorem Provers and AI have both risen to prominence concurrently and complementarily: the confidence offered by the formal paradigm strongly incentivises training, benchmarking and deploying models to reason formally, and improvements in AI are strongly influencing the development of formal mathematics. The demand for formal verification has never been greater. Yet, while AI models are proving themselves increasingly capable of autonomously verifying proofs in interactive theorem provers like Lean, they continue to depend heavily on over a decade’s worth of formal infrastructure built through open-source collaboration and carefully curated by human maintainers. For formal mathematics to develop sustainably, important (if subtle) distinctions must be drawn between formal verification and canonisation. While both serve valuable purposes, these purposes are distinct, and the capabilities of models to serve them differ starkly. My talk will explore the nuances of doing formal mathematics in the age of AI, motivated and illustrated largely by joint work on formalising sphere packing in dimension 8 with Birkbeck, Lee, Ma, Mehta, Poiroux and Viazovska.