Formalizing US Tax Code (Using Lean)

Researchers used the Lean proof-checking programming language to formalize the entire US Internal Revenue Code and identify errors in its text, discovering 138 real drafting mistakes including broken cross-references, typos, duplicate provision numbers, and unclosed parentheses. This work, part of a global effort to formalize legislation as machine-readable code, aims to catch contradictions and mechanical errors that humans miss, and was validated by testing translations against IRS-provided examples. The approach also successfully rediscovered known tax loopholes like the backdoor Roth conversion, suggesting it could identify previously unknown loopholes in the tax code.