Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)