Pure Maths Colloquium: Kevin Buzzard

We all know that computers can grind out computations, and that sometimes the way to finish a proof is to grind out a computation. A famous example is the proof of the four colour theorem. These so-called “computer-assisted proofs” are powerful tools in some areas of mathematics. But what if you study objects which cannot be usefully stored in a computer? It turns out that computers are coming for you anyway! Modern AI techniques, and so-called computer proof assistants, are ways of using computers to generate not data but mathematical ideas. Computers cannot yet replace pure mathematicians, but I believe that we are moving towards a future where computers will be helping mathematicians not just to compute, but to reason. I’ll give an overview of the area as it stands, suitable for pure mathematicians. No computer background will be assumed.