Broad Perspectives on Formal Mathematics
Formal Mathematics and AI at Carnegie Mellon · New York City (NY), United States · 18 September 2026
Proof assistants are not new: the first were built nearly sixty years ago, and mathematicians have been formalising serious mathematics in them since long before AI entered the picture. For most of that history, the benefits of doing so were vast and diverse, extending well beyond the obvious one of certifying correctness: formalisation built libraries, developed theory, eased collaboration, and, perhaps most valuably, improved our understanding of the mathematics being formalised. AI has brought proof assistants renewed attention, but it has also narrowed the emphasis onto correctness, and onto trust, as the chief benefit of working formally. In this talk, I will trace how the world of formal mathematics came to be what it is, describe what autoformalisation has made possible, and argue that important, if subtle, distinctions must be drawn between formally verifying mathematics and canonising it.