Well, the statement can be the 500k line part if it's generated with an LLM. But I think some people miss the point of Lean when they use LLM like that.