Humans use computers to do gigantic calculations which would be impossible to do by hand – for example, weather prediction. But could an AI go beyond that and come up with a proof of a theorem which has stumped humankind? Could computers suggest how to attack problems, searching knowledge bases for known results?
As automatic and interactive computer theorem provers become more powerful, should mathematical researchers begin to worry that they will soon be out of a job?
Kevin is Professor of Pure Mathematics in the Faculty of Natural Sciences at Imperial College London. His expertise lies in algebraic number theory and currently works in the area of formal proof verification. He has given lectures for the Royal Institution and for Microsoft Research.
