Anatomy of a formal proof