Formalizing US Tax Code (Using Lean)

Yesterday, we verified that known tax loopholes could be identified using a Lean search. Today, we set out to formalize the entire Internal Revenue Code to hunt for unknown loopholes (bugs).

The Details

Pointing a proof checker at statutes

Lean is a programming language whose type checker can also check mathematical proofs: if Lean accepts a proof, every step follows from the definitions, with nothing taken on trust. An earlier post discussed how far that kind of formalisation can reach in law, [ 1] and yesterday we used it on the retirement-account rules, where a blind search rediscovered the backdoor Roth.

This work is part of global-law global-law, a CC0 repository of versioned legislation and case law.

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. In particular, we can catch mistakes in the text, and see what the rules allow, including what they allow by accident. To do so, we translated each section of the law into Lean, staying close to the statute’s own words, and tested it against the worked examples the IRS prints in its forms and instructions.

1. The tax law’s text has 138 drafting mistakes The tax law is Title 26 of the US Code. Its official text is published as structured data by the Office of the Law Revision Counsel, the office of the House of Representatives that compiles the Code.

We used the release current to 3 November 2026.

A parser then reads every cross-reference, including the ones written in words (“paragraph (2) of subsection (b)”, “such subparagraph”, “sections 922 through 927”), which carry no hyperlink. Lean checks each one. Does the provision it points to exist? Is it still in force? (verifiable via our versioned history) The checks run as a test suite, which fails whenever a new release adds a fault the last one did not have.

The suite reports 257 findings, each checked by an AI agent against the official text and its editorial notes: 98 intended (rules for past periods, and provisions enacted but not yet in effect), 21 false alarms in the editors’ own hyperlinks, and 138 real faults:

• Fault
• Count
• Example

Reference to something since repealed, moved or rewritten, with no conforming change 67 §1(f)(7)(A) cites a rewritten provision §168(n)(2)(G) cites a moved provision Typo, wrong subdivision or unnamed Act 24 §1400Z-2(f)(1) cites the wrong subsection §72(t)(2)(A)(viii) has a typo in a citation Wrong level word 8 §9818(a)(1)(A) calls a subsection a paragraph Two provisions with the same number 9 §1202(b)(4) appears twice §45X(d)(4) appears twice Parentheses that never close (13 footnoted by the editors, 17 not)

• 30
• §165(h)(1) leaves a parenthesis open
• §38(c)(6)(C) leaves a parenthesis open

Each of the 138 has a certificate: a short Lean statement that carries its evidence from the official XML and proves the fault. For a dead reference, the evidence is the full list of what does exist under the cited provision. Lean re-checks all 138 in about two and a half minutes.

Our record of the US Code is a git history, one commit per public law, [ 5] so each fault can be traced to the law that wrote it. For Title 26 the record reaches back to the 1994 edition.

This check is cheap to repeat. Run against each new release of the Code, it flags a new mistake as soon as it appears, and names the law that caused it.

2. Rewriting the income tax as code that can be checked Next we wrote down what the law calculates: the 2025 federal income tax for one household, meaning the numbers on Form 1040, including the changes made by the One Big Beautiful Bill Act in July 2025.

• [
• 6],
• [
• 7]
• We did it in four parts:

Income, down to adjusted gross income (AGI). AGI is total income minus a few items, such as IRA contributions and student-loan interest. Most other tax rules depend on it.

Deductions: the standard deduction or itemized deductions, and the new deductions for tips, overtime, car-loan interest and people over 65.

The tax itself, including the alternative minimum tax (AMT), a second calculation that stops high earners from cutting their tax too far with deductions.

Credits, such as the child tax credit and the earned income tax credit (EITC), a credit for people on low and moderate wages.

We used AI to translate the statute into Lean. This is the lossy step, therefore we reinforce it with the following measures:

Each part is tested against figures the IRS publishes (the Tax Table, the EITC table, the worksheets and the examples in its publications), and checked against three independent tax programs on 5,000 households (section 3).

A second agent, which did not write that part, reviews it adversarially, looking for errors and for cheating, such as code written to pass the tests rather than to follow the statute.

What Lean ultimately adds is proofs that cover every input instead of a sample. For example, it proves that the SALT cap and the car-loan and overtime deductions never grow when income rises, at every income and for every filing status.

The comparison with other tax software helps us catch logical errors. That is how we caught two mistakes in our own model. It is also how we found bugs in the other tools that were logical rather than arithmetic: Tax-Calculator gives the EITC to separate filers without checking whether the spouses lived apart, and UsTaxes never attaches Schedule C to the 2025 return, so self-employment income disappears.

Writing the model turned up five things:

The published Code mixes 2025 and 2026 law.

In six places the consolidated Code already shows the 2025 Act’s amendments that start in 2026. Read without the effective-date notes, it gives the wrong 2025 tax: the AMT phase-out at 50% instead of 25%, a charity floor and a cap on itemized deductions that do not yet apply.

The same Act rounds in opposite directions.

The new tips and overtime deductions shrink by $100 for each full $1,000 of income over the limit, so one more dollar of income can cost $100 of deduction. The new car-loan deduction shrinks by $200 for each $1,000 “or portion thereof”, which rounds the other way, so it runs out $999 sooner than the round numbers suggest.

A married couple can deduct more state and local tax by filing separately.

The deduction for state and local taxes (SALT) is capped, and the cap shrinks as income rises: by 30 cents for each dollar over $500,000 on a joint return. On a separate return, the law halves the cap after shrinking it, so it shrinks by only 15 cents a dollar. A couple earning $300,000 each can deduct up to $25,000 on two separate returns, but only $10,000 on one joint return.

The Tax Table is not the tax formula.

Most people with taxable income under $100,000 look up their tax in the IRS Tax Table instead of working it out. The table differs from the formula in the law by between −$5 and +$6, and Lean proves that range for every income under $100,000 and every filing status.

One dollar can cost $8,046.

Some benefits switch off at a line instead of fading out. A family with three children can lose its whole EITC, up to $8,046, because its investment income is one dollar over $11,950. The saver’s credit, a credit for retirement saving, works the same way: a couple who each put $2,000 into retirement accounts gets $2,000 at an income of $47,500, and $800 at $47,501.

3. Testing it against tax software people already use A model is only useful if it gives the right answers. To check ours, we built 5,000 sample households and worked out each one’s 2025 tax four ways: with our model, and with three tools built by other teams, independently of each other and of us:

PolicyEngine-US, an open-source model that researchers and policymakers use to estimate how tax and benefit changes affect households; [ 8] Tax-Calculator, the Policy Simulation Library’s open-source model of the