Computer theorem provers (which know the axioms of mathematics and can check proofs) have existed for decades, but it's only recently that they have been noticed by mainstream mathematicians. Modern work of Tao, Scholze and others has now been taught to Lean (one of these systems), and (following notes of a Stanford course by Taylor) I've begun the long journey towards teaching Lean a proof of Fermat's Last Theorem. After an overview of what these systems are and what they can currently do, I'll discuss why I'm now motivated to work in this way, and why I never want to go back to pencil-and-paper mathematics. This talk will be independent of, and have very little overlap with, my public lecture, but like the public lecture will not assume any expertise in computer science.