Byron Cook

For over two decades, Professor Byron Cook has been trying to get computers to prove mathematical theorems. In other words, getting machines to verify, with absolute certainty, whether something is true or false. He says it’s the kind of work that used to make for awkward dinner party conversations. “Throughout my career, I’ve had a very hard time describing to people who weren’t deep technologists what I did. But now, it’s quite easy because people have seen for themselves incorrect answers to questions,” says Cook, who leads the AWS Automated Reasoning Group and holds a professorship at University College London. Recently elected as a Fellow of the UK’s Royal Academy of Engineering for his pioneering work, Cook is finally seeing his obscure mathematical field become something people encounter every time they use AI tools, although they might not realise it.

With GenAI chatbots and image generators regularly producing – or hallucinating – incorrect outputs, the general public has gained a new appreciation for the limitations of these intelligent systems. “They’ve seen it firsthand. These AI tools aren’t as foolproof as people might have thought,” says Cook.