Abstract: Proof checking the full book of Landau

Bert van Benthem Jutting

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.