I think you've nailed a subtly — and a major doubt — I've been been trying to articulate about code helpers from LLMs from day one: the difficulty in programming is reducing a natural language problem to (essentially) a proof. I suspect LLM's are great at transferring style between two sentences, but I don't think that's the same as proof generation! I know work is being done I this area, but the results I've seen have been weird. Maybe transferring style won't work for math as easily as it does for spoken language.