Kevin Buzzard found computer-based formal mathematics to be a novel approach and much more enjoyable than working with paper and pencil, which drew him in.

“So the-- but, but by that stage, I kind of got hooked 'cause I realized that there was this weird new way of doing mathematics. I'd never really seen anything like it before, and I started to realize that actually doing mathematics in the software, even though it was very basic mathematics, was a huge amount of fun, you know, very different to doing it on paper and pencil.”