Date/Time Date(s) - 06/02/20263:30 pm - 4:30 pm
Speaker: Chris Kapulkin (Western University)
Location: Hamilton Hall, Room 305
Title: Is mathematics obsolete?
Abstract: The advent of computers since the 1940s gave mathematicians new tools for performing computations and formulating new conjectures. One thing it hasn’t done, however, is fundamentally change the nature of mathematical research. Papers written in 2026 don’t differ in a significant way from those written a century ago. This situation may be poised to change as the role of computers is changing – new tools, including: formal verification, automated reasoning, and machine learning are becoming ever more present in mathematical research.
This talk will survey some of these recent developments, reflecting on what might lie ahead, with a focus on formal verification, i.e., the process of checking correctness of proofs via software known as proof assistants. I will include a live coding demo of a simple proof in the Lean proof assistant, so feel free to bring your laptop if you’d like to follow along (or catch up on your emails, I get it…).
No familiarity with Lean, or any other software, will be assumed. The talk should be accessible to (undergraduate and graduate) students and faculty alike.
Coffee will be served in Hamilton Hall, Room 216 at 3:00pm. All are welcome.