Michalik Distinguished Lecture: Computer-Assisted Thinking

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.