Formalizing the US Tax Code

The work applies Lean, a proof-checking programming language, to the Internal Revenue Code: first checking statutory cross-references and then encoding the 2025 income-tax rules. Of 257 apparent reference problems in the Code, 138 were verified as genuine drafting faults, including dead references, duplicate provision numbers, and unclosed parentheses. The tax model also exposed timing and calculation quirks, such as amendments shown in the consolidated Code before they take effect and sharp deduction or credit cliffs. Tested on 5,000 households against three independent tax tools, it agreed with PolicyEngine on all but seven cases, where differences were at most $11; the comparison also revealed bugs in other software and corrected two errors in the Lean model.

Automated searches over nearly 196,000 returns and decades-long family plans rediscovered established strategies, including Roth conversions and separate filing to qualify for deductions. The searches also found a narrow Social Security tax opportunity not located in practitioner guidance: some couples living together can owe less by filing separately, because a working spouse’s wages can push benefits to the taxable maximum on a joint return while a retiree’s separate income does not. In one example, separate returns reduce tax by $1,482, though the advantage disappears at higher wages. The findings show how formalizing tax rules can reveal both mechanical mistakes and strategies hidden in the interaction of provisions; the supposedly unreported opportunities are not established as genuinely new.