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…