On the one-hand side, it's really impressive how LLMs drive mathematics forward, and this pace is only accelerating very quickly. At the same time, most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter). LLMs do not care about "elegance" the way human beings do, which is a big advantage. LLMs for mathematics is such a great fit on many levels…
Sure they care about elegance, or at least brevity. Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems. It doesn't mean they are perfect at it though.
First time I heard that, and I doubt it. Don’t customers pay for output tokens? If so, why would a company specifically spend time training their LLM to generate fewer?