alt Hacker NewsJust reading chain of thought traces for Agda (I'm using Qwen 3.8-Flash-Next) and it's struggling so hard with just the syntax, long before it can struggle with semantics or type errors.
Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.
Yeah I know this pain. I actually have had some success by giving the agent a style guide for Lean that is strictly not conventional. The nice syntactic shortcuts and different modes that make Lean more ergonomic for humans, in my experience, actually make it easier for an agent to trip itself up.