This is a really important point. Honest question, have we ever seen LLMs doing or creating something truly novel or innovative? I mean they can patch together proofs (or functions/programs - same thing via Curry-Howard) by broad searching existing lemmas they can piece together, but create something truly novel and insightful? That seems to be the limit?