To be clear: I’m aware the LLMs are solving problems. I’m just saying that what enables that whole research revolution is Lean. We wouldn’t be seeing all those results without it. I would like to see it acknowledged when people are talking about LLMs solving maths. The same way I think we should acknowledge the humans who are guiding and prompting the LLMs. I don’t think that necessitates to move a goal post