IMPA - O Instituto de Matemática Pura e Aplicada

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. The view of AI will be neither all rosy (I will introduce bullshit as a technical term) nor all gloom. My qualifications: I've coauthored an online textbook on the Agda proof assistant, available at plfa.inf.ed.ac.uk, and I've spoken on AI at the Edinburgh Fringe.

Bio and photos here: https://homepages.inf.ed.ac.uk/wadler/bio.html.