In this talk, I will look back at the time when we were working on automating the whole book of Landau in Automath. I will discuss the challanges we faced and how we overcame some of these challenges.