Math Education Seminar: Why care about mathematical proof in the age of AI?

Kenny Easwaran, UCI

Title: Why care about mathematical proof in the age of AI?

Abstract: Since the early 20th century, philosophers have debated the relationship between informal proofs of the sort mathematicians have produced in their work for centuries, and the formalized proofs that appear in the branch of logic known as "proof theory". In the early 21st century, these questions grew more pressing with the development of computer verification systems like Isabelle, Mizar, and Lean, which enabled mathematicians to more efficiently (but still slowly) translate informal proofs into formalized ones. Over the past year AI systems have suddenly upended the relationship of mathematicians to both formalized and informal proofs, by generating new informal proofs (like OpenAI's announcement of May 20 of a new bound for the planar unit distance problem) and new formalizations of long and difficult informal proofs into formalized proofs (like Anthropic's announcement on Sept. 4 of a formalization of Wiles's proof of Fermat's Last Theorem), and the combination (like OpenAI's announcement on Sept. 8 of a novel formalized proof of a counterexample to existence and smoothness of solutions to the Navier-Stokes equation). In this talk, I will discuss the relevance of the work of various philosophers of mathematics to the novel situation we are confronted with, and the questions this raises about the goal of mathematics as a human endeavor.