Computer Algebra and the Formalisation of New Mathematics

This lecture describes the formalisation of a celebrated new mathematical result that appeared in 2023: an exponential improvement for diagonal Ramsey numbers. I gave this talk in the department of mathematics at Cambridge in November 2024, and a similar talk at the SC-Squared Workshop in Nancy, France, that June. The slides are not especially visible but can be viewed here: www.cl.cam.ac....