Although proof has been central to mathematics from ancient times, our understanding of what a proof is has evolved through the years. In the seventeenth century, Isaac Newton proved things about infinitely small quantities; two hundred years later, Georg Cantor proved things about quantities that are infinitely large. Some proofs rely on calculations that are too long to carry out by hand; some collaborative proofs are too large to be understood by any one person; and now, we can even write proofs that a computer - or AI - can understand and evaluate. Join Jeremy Avigad, Professor of Philosophy and Professor of Mathematical Sciences at Carnegie Mellon University, as you experiment with contemporary proof-checking technology and explore recent developments that challenge our understanding of mathematical proof.

A talk given at The National Museum of Mathematics (MoMath) on 6 November 2024.

Video link