This is the start of Chapter 15, about interactive theorem provers (ITPs).  In this episode, I talk about the difference between fully automatic and interactive provers, and my plan to discuss and compare several different ITPs, in future episodes of this chapter.