Proving Theorems with Computers (AMS Notice, Kevin Buzzard) [pdf]

I'm really happy with the framing of this article, and with the nuance in discussing other ITPs and the history of ITPs!