Lexifina 用 Lean 形式化美国税法，发现 138 处起草错误与 3 个新税收漏洞

Lexifina 将美国税法 Title 26 全文翻译成 Lean 并用证明检查器审计，在 2026 年 11 月 3 日版本中发现 138 处真实起草错误，包括失效引用、重复编号和未闭合括号。