I'd definitely say it understands those theorems with respect to the metamath formal system then. The next question is what it understands the proofs with respect to.