Hear from Phil Wadler, one of the pioneers of Programming Language research, who contributed a few pivotal ideas in Computer Science and in the design of languages such as Haskell, Java, and Xquery. This time, he will be speaking about Proof Assistants and AI. The talk is suitable for a wide audience, anyone interested in formalisation of Mathematics and Computer Science, as well as the future of Gen AI in Maths and Computer Science.
Proof assistants, including Lean, Rocq, and Agda, are making inroads in both computing and mathematics. This talk will explain why. It will also consider recent developments in—what else?—AI, and how it relates to proof assistants.