Why formalise mathematics in 2027?
Colloquia Seminar
26th October 2026, 4:00 pm – 5:00 pm
Fry Building, TBC
A growing number of people are having fun explaining mathematics to computers using proof assistant softwares. This process is called formalisation. In this talk, I’ll show what formalisation looks like, describe what kind of things it teaches us, and how it could even turn out to be useful. This landscape is rapidly changing as part of the global generative AI disaster, so I will also include a discussion of how I hope those activities can stay relevant in 2027 and beyond.
Organiser: Matthew Tointon
Comments are closed.