I can't comment on your detailed knowledge of the state of the art, but your points resonate (particularly because I have tried to generate Julia and Lean code).

So, as with any less informed user reviewing LLM output, what you say definitely sounds plausible and correct.