用 Lean 把美国税法形式化，找出 138 处起草错误

📋 概述

Lexifina 做了一件听起来荒谬但方法很硬的事：把美国税法典（Title 26）逐条翻译成 Lean，让证明检查器来查漏洞。Lean 的类型检查器同时能做证明检查，只要接受，每一步都从定义推出、不依赖任何信任。他们此前用盲搜在退休账户规则里重现了 backdoor Roth，这次则把整部税法形式化，并用 IRS 表格和说明里的算例做对照测试。第一个结果是：法条正文里存在 138 处起草错误，而这些正是人和工具都会漏掉的机械性差错。