We are pleased to announce that our 2024 Michalik Lecture will be given by Professor Heather Macbeth. The doors for the event will open at 3 PM. Following the talk a reception will be held in the Frick Fine Arts Cloister after the talk has concluded until 5:30 PM.
Title: Computer-Assisted Thinking
Abstract:
After decades of work by mathematicians called "theoretical computer scientists", computer systems for formalization -- expressing proofs as strict chains of logical reasoning, down to the axioms -- are now powerful and user-friendly enough for modern research mathematics. And indeed, instances of hot-off-the-press theorems being formalized are starting to accumulate, including Hales' proof of the Kepler conjecture, Clausen-Scholze's work on condensed mathematics, and Gowers-Green-Manners-Tao's proof of the Polynomial Freiman-Ruzsa conjecture.
These developments suggest new paradigms for the interaction of mathematics and computation. Computer formalization systems (called ITPs, for "interactive theorem provers") can explain to us what our "abstract nonsense" means, and force us to explain to them what we mean by "routine" proofs; in both cases an implicit algorithm is made explicit. ITPs are the ideal vehicle for very computational proofs -- so much so that the line between "brute force" proofs and "principled" proofs begins to blur. And seemingly in contrast to this, ITPs may nudge us toward a different style of mathematical discovery, less reasoned and more intuitive.
Location and Address
125 Frick Fine Arts Building
Speaker Information
Heather Macbeth, Fordham University