Lexifina 用 Lean 形式化美国税法，发现起草错误与税收漏洞
热点事件持续更新
Lexifina 用 Lean 形式化美国税法，发现起草错误与税收漏洞
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
Lexifina 将美国国内税收法典（Title 26）全文翻译成 Lean 形式化语言并用证明检查器审计，在 2026 年 11 月 3 日版本中发现 138 处起草错误（如失效引用、重复编号、未闭合括号）以及 3 个新的税收漏洞。此前他们已验证可以用 Lean 搜索找出已知的税收漏洞，本次是对整部税法的形式化以寻找未知漏洞。 需要说明的限制：起草错误的分诊和审核由 AI 代理对照官方文本完成，尚未经律师或注册会计师复核；其模型仅覆盖 2025 年个人家庭报税的个人所得税部分。
AI 根据报道生成 · 4 分钟前更新
最新进展11月14日 23:41
Lexifina 用 Lean 形式化美国税法，发现 138 处起草错误与 3 个新税收漏洞报道时间线
沿着报道，了解事件的不同侧面。
11月14日
- Hacker NewsLexifina 用 Lean 形式化美国税法，发现 138 处起草错误与 3 个新税收漏洞
Lexifina 将美国税法 Title 26 全文翻译成 Lean 并用证明检查器审计，在 2026 年 11 月 3 日版本中发现 138 处真实起草错误，包括失效引用、重复编号和未闭合括号。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。