AI, Proofs, and Programs

AI is transforming mathematics, raising profound questions: Can we trust AI-generated proofs? Do we understand them? And what role will mathematicians play in this new era? This talk explores these questions through the lens of proof checking, formal systems, and the elegant Curry-Howard correspondence—a deep connection between logic, computation, and the nature of mathematical truth.