Will Computers prove theorems?

Strachey Lectures

Kevin Buzzard: Will Computers prove theorems? Will computers one day replace human mathematicians? Is this just around the corner, or decades away? Can neural networks spot patterns which humans have missed? Currently language models are great for brainstorming big ideas but are very poor when it comes to details. Can integrating a language model with a theorem prover like Lean solve these problems? Is the modern mathematical literature riddled with errors, and is it feasible to hope that a machine might find and even fix them? Is it possible to teach a computer the proof of Fermat's Last Theorem? And what do mathematicians make of all this? I'll talk about how modern developments in AI and theorem provers are beginning to affect mathematics.