开发者观察：AI 智能体编写 Lean 仍难胜任依赖类型编程

开发者观察指出，当前 AI 智能体在依赖类型编程上表现不佳，即使使用 Lean 定理证明语言，也难以适应依赖类型范式。其直觉仍过度倾向命令式编程，反映出编程智能体在形式化验证等高度抽象领域的能力短板。