LeanCat-astrophe: Why Category Theory Is Where LLM Provers Go to Struggle
A developer can understand what a software function should do, write something that looks reasonable, and still fail because the surrounding codebase expects a particular interface, naming convention, object hierarchy, or sequence of calls. Giving the developer four independent attempts may eventually fix a misplaced bracket. It does little when the real problem is that they do not know which internal abstraction the system expects. ...