Formalizing the US Tax Code in Lean to Identify Drafting Errors and Loopholes

A team of researchers identified 138 drafting mistakes in the US tax code by translating the statutes into Lean, a programming language whose type checker can verify mathematical proofs. By treating the law as a set of verifiable definitions, the team was able to automatically flag broken cross-references, typos, and inconsistent subdivisions that exist in the official text of Title 26 of the US Code.

The table provides specific examples of the drafting errors found during the initial auditing phase.

Automated Auditing of the Internal Revenue Code

The researchers used a parser to read every cross-reference in the tax law, including those written in plain text like 'paragraph (2) of subsection (b)'. Because these references lack hyperlinks in the official text, they are prone to becoming 'dead' when the law is updated.

Lean verified each reference against a versioned history of the Code. The test suite reported 257 findings, which an AI agent then categorized. While many were intended rules for past periods, 138 were confirmed as real faults, such as citations to moved provisions or incorrect subdivision names.

Chart drawn by HN Digest from figures reported by lexifina.com; values are shown as written in the source.

“Our argument is that pointing AI and a proof checker at a versioned record of the law finds the contradictions and mechanical mistakes that people miss.”

— Formalizing the US tax code | Lexifina

Rewriting Tax Logic as Verifiable Code

To move beyond simple text checks, the team rewrote the 2025 federal income tax calculation into Lean. This involved modeling four distinct components: income (down to adjusted gross income), deductions, the tax calculation (including the alternative minimum tax), and credits.

This diagram visualizes the scale and organization of the formal Lean model used to represent the tax code.

Because translating natural language into formal code is a 'lossy' step, the team reinforced the model by testing it against IRS-published figures and three independent tax programs. They also employed an adversarial AI agent to review the code for 'cheating'—logic designed to pass tests without actually following the statute.

Discovering Hidden Loopholes and Software Bugs

The formal model allowed the team to run a 'blind search' for tax planning strategies. This revealed three novel loopholes not found in practitioner guides, such as a specific window where a couple living together could save money by filing separately due to how Social Security benefits are capped.

The project also exposed discrepancies in existing tools. For example, one popular tax software failed to attach Schedule C to returns, causing self-employment income to disappear. Additionally, the team proved that the IRS Tax Table is not a perfect reflection of the law's formula, showing a variance of up to $6 for many filers.

This table highlights the specific loopholes and software bugs uncovered by the research team.

Limitations and the Role of Human Interpretation

While Lean provides a rigorous check of the law's literal text, the project highlights a significant boundary: the 'spirit' of the law. A machine can prove what the text allows, but a human judge remains the final arbiter of whether a specific interpretation is legally acceptable in a court of law.

Furthermore, the transition from statute to code remains a manual process of interpretation. The researchers noted that while Lean can prove that certain deductions never grow when income rises at every possible input, the initial translation of the law into those definitions still requires human oversight to ensure the formalization accurately captures the legislative intent.