Comment by gsf_emergency

Sorry to go off on what may seem to be a tangent (equivocating only bcos i struggle to get the pt across succinctly?)

This too could form the basis of a productive skepticism towards the usefulness of coding agents, unlike what has caught attention here. (Referring specifically to the post by tptacek)

For example, we could look at feedback from the lisp community (beyond anecdata) on the usefulness of LLMs? Since it's what one might call "syntax-lite", a lack of true generalization ability ("no possible world model for an unavoidably idiosyncratic DSL-friendly metalanguage") could show up as a lack of ability to not just generate code, but even to fix it..

Beyond that, the issue how much the purported world-shattering usefulness of proof assistants based on say, Lean4, must depend on interpolating say, mathlib..

In short, please link the papers :)

>There are two follow up papers showing the representations are "entangled", a euphemism for statistical garbage, but I can't be bothered at the moment to find them.