Gwern Branwen,
formal methodsleansoftware engineeringcoding agents
Gwern's proposal is useful because it asks a sharper question than "can agents write more code?" It asks what kind of software substrate would let code, proofs, docs, tests, and design intent scale together instead of drifting apart as the system grows.
That belongs near the agent-workflow links. If code generation keeps getting cheaper, the bottleneck moves toward specification, review, interfaces, invariants, and machine-checkable confidence. Lean is not a magic management layer, but this is the right direction of pressure: make the important claims in a codebase inspectable by tools, not merely implied by convention.