Comment by 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.