Undergraduate Student Seminar (Pi Mu Epsilon talk)- Proof Assistants and the Future of Math (feat. Lean)

Title: Proof Assistants and the Future of Math (feat. Lean)
Speaker: Apurva Nakade
Date and Time: Friday, April 25, 4:00-5:00
Place: Rome Hall, Room 771

Abstract: With the recent buzz around AI systems tackling math problems, there's growing interest in how computers might support the way we explore and verify mathematics. Behind the hype are proof-checking systems mathematicians and computer scientists are already using today. In this talk, we’ll explore the Lean theorem prover, a tool that helps mathematicians write precise, checkable proofs with the help of a computer. Through live demos, we'll see how Lean works and why it’s becoming a favorite among a new generation of mathematicians. If time permits, we’ll also explore deeper foundations, including type theory and the Curry-Howard correspondence, which links logic and computation in elegant ways.

Bio: Apurva Nakade is a senior lecturer in the Department of Applied Mathematics and Statistics. His primary interests revolve around improving math education and discovering methods to lower barriers and enhance retention in entry-level math courses. He actively participates in the redesign and adaptation of courses to emphasize modeling and data-driven approaches. Additionally, he is involved in the development and utilization of open-source educational resources for teaching math.

His research focuses on algebraic topology, type theory, and mathematical formalization. Nakade plays an active role in expanding the math library for the Lean Theorem Prover, an open-source project that brings together mathematicians and computer scientists worldwide. One of the project’s goals is to develop automation and educational tools for mathematicians and mathematics students.

**

This talk is open to everyone.  Mathematics majors and minors are especially encouraged to attend.  You are also encouraged to come to Phillips 704 starting at 3pm where we will have refreshments.