Lawrence Paulson: Formalising Advanced Mathematics in Isabelle/HOL

The formalisation of mathematics is now a reality. A number of recent and highly sophisticated papers have been formalised, in some cases before human referees had time to submit their reviews. Most of this work has been done using the Lean proof assistant. The speaker will discuss the accomplishments and conclusions of a six-year research project devoted to formalising advanced mathematics using Isabelle/HOL and highlight some special considerations arising from that choice.