Il professore, che auspica un massiccio futuro utilizzo del PC come strumento per controllare ma anche per formulare strategie di soluzione dei teoremi/congetture, è Kevin Buzzard.
https://www.youtube.com/watch?v=Dp-mQ3HxgDEIl video è piuttosto noiosetto. Spiega le sue ragioni e presenta gli sviluppi fatti con Lean (il programma che ritiene più promettente) negli ultimi due anni. In pratica gli studenti lo stanno aiutando ad inserire in modo corretto le formalizzazioni matematiche in modo che Lean possa capirle ed utlizzarle (insomma una sorta di database).