Lean Agent

lean-agent 用 Lean 4 显式化代码前置条件，以 Invariant Enforcement Score 衡量假设是约定、运行时检查还是类型结构，并迭代修改到分数稳定。ledger 示例把 13 行转账逻辑从 IES 0.00 提到 1.00，补上账户存在、正金额和余额足够等检查；Lean 证明仍使用 `sorry`，所以它的承诺是让假设进入类型签名而非已完成形式化证明。`enforce` 与 `score --min-ies 0.80` 可直接做 CI gate。