[oh_my_goodness]

I think it's reasonable to ask whether LLMs formalize theorems correctly. And I'm not sure that saying "this one is easy" answers that question.