I laud the Metamath proof checker and its excellent book.  I am also looking for suggestions on what to discuss next, as I am ready to wrap up this chapter on proof assistants.