Lexifina 用 Lean 形式化美国税法并查找漏洞

Lexifina 将美国税法逐条转为 Lean 形式化模型，用于检查交叉引用、验证 2025 年联邦所得税计算并搜索可能的税务漏洞。团队在 2026 年 11 月 3 日版本的 Title 26 中确认 138 处真实错误，并通过对 5,000 个家庭的四套计算结果比较，发现 3 个此前未见实务资料的税务问题。