d(h)sign
Computers are now better than humans at logical games and puzzles such as Sudoku, Chess, Go and so on. Mathematics can also be framed as a logical puzzle game. When will computers become better than humans at developing new mathematics and proving new theorems? Certainly this has not happened yet, but in the last few years there has been an explosion of activity, with tools such as neural networks, language models and computer theorem provers all being involved. I will survey the state of the art. Research mathematicians can currently sleep easy -- but for how long? The talk is suitable for a general scientific audience: no background in modern mathematics or computer science will be assumed.
Kevin Buzzard is Professor of Mathematics at Imperial College, London. He has held research positions at the University of Cambridge, the Institute for Advanced Study in Princeton, and Harvard University. His work has been recognized with the Whitehead Prize and the Senior Berwick Prize awarded by the London Mathematical Society. In 2017, he launched a formalization project and blog involving the Lean theorem prover, and has since promoted the use of computer proof assistants in future mathematics research. He gave a special plenary lecture at the 2022 International Congress of Mathematicians on the rise of formalism in mathematics, and is currently working on a formalization of Fermat’s Last Theorem in Lean.
You can find more information about speaker Kevin Buzzard here: https://profiles.imperial.ac.uk/k.buzzard