I talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.