Formalizing the US tax code

A Lean-based formalization of Title 26 of the U.S. Code has identified 138 drafting faults in the current tax statute, including 67 references to provisions that were repealed, moved or rewritten without conforming changes, 24 typos or wrong subdivisions, 30 unclosed parentheses and nine duplicated provision numbers. The project, part of the CC0 global-law repository, translated each section of the law into the Lean proof language and tested it against IRS worked examples, using structured text from the Office of the Law Revision Counsel current to November 3, 2026. An AI agent reviewed 257 flagged findings and classified 98 as intended, 21 as false alarms in the editors' own hyperlinks and 138 as real faults, each backed by a Lean certificate that re-checks in about two and a half minutes. The effort matters because proof-checking a versioned record of the law can surface contradictions and mechanical errors that human review misses, including rules that apply by accident. Next to watch is whether the test suite catches new faults in future releases and whether formalization extends beyond cross-reference checks toward the substantive loophole hunt demonstrated on retirement-account rules.