Formalizing US Tax Code (Using Lean)

Comments

Formalizing the US tax code

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).

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.[2]

This work is part of global-law, a CC0 repository of versioned legislation and case law.[3] 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.[4] 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:

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 federal income tax;[9]
• UsTaxes, a free, open-source app for preparing your own tax return.[10]

Two thousand households were ordinary. The other 3,000 were deliberately awkward: couples filing separately, widows and widowers, students, people with tips or overtime, IRAs and health savings accounts, education and saver's credits, and incomes over $1 million with large investment gains.

Our model and PolicyEngine-US agreed on every figure for 4,993 of the 5,000 households. The other seven differ by at most $11, all in the EITC: our model reads the IRS's printed EITC table, while PolicyEngine-US uses the formula behind it.[11]

Tax-Calculator gave the EITC and the child and dependent care credit to married people filing separately without checking that the spouses lived apart, which the law requires. It also computed no AMT for one high-earning separate filer, where two other calculators computed $14,881.

UsTaxes had 14 bugs, each confirmed by recalculating an affected household. It drops self-employment income without a warning, because its 2025 return never attaches Schedule C, the form for business income. Its child-care credit never reaches the return. Its age test for the EITC always passes. And its self-employment tax counts a spouse's wages against the cap on Social Security tax. Together, these bugs affect about one ordinary household in six.

The comparison caught two mistakes in our own model too. We had not counted self-employment profit toward the 20% deduction for small-business income. And we always took the larger of the standard and itemized deductions, although the law lets you choose to itemize a smaller amount, which can pay when it lowers the AMT. With that fixed, one household owed $2,070 less. Both mistakes showed up because two independent tools agreed with each other and not with us.

4. A search found the loopholes tax advisers already use

With a model that matches the reference software, we used it as we had used the retirement rules: as the oracle for a search that knows no tax planning. The first search tried ordinary choices for each of the 5,000 households, 195,787 returns in all:

• file separately, and which spouse holds which investments, pays which bills and claims which children;
• contribute to an IRA;
• earn a little less;
• realize more or less gain.

The second search used a multi-year family model, which adds the kiddie tax, trust taxation, Roth conversions, required withdrawals, gifts and death. It tried about 30,000 plans for four families over 34 to 47 years.

Everything large that the two searches found is already in the planning literature:

As with the backdoor Roth, none of these was described to the search. It found them because the rules, written down plainly, permit them.

5. Novel loopholes we found

Three results did not turn up in practitioner sources, IRS guidance or tax-software forums.

Filing separately can cut tax on Social Security, even for a couple living together. The standard advice is that a couple living together should never file separately when one draws Social Security.[16] A separate filer who lived with their spouse gets no base amount at all. But taxable benefits are capped at the lesser of 85% of benefits or 85% of provisional income,[17],[18] and the search found couples for whom that cap makes separate returns cheaper. On a joint return the working spouse's wage counts in provisional income, so a moderate wage already pushes the benefits to the 85% maximum. On a separate return the retiree's benefits are measured against the retiree's income alone. With $48,000 of benefits and a $60,000 wage, the couple owes $7,050 jointly and $5,568 separately, $1,482 less. A second reviewer recomputed it by hand and got the same answer. At a $100,000 wage the result flips, so the window is real but narrow.

Wages on one return, investments on the other. The 3.8% tax on investment income applies to the smaller of the investment income and the excess of income over $250,000 jointly, or $125,000 on a separate return.[19] On a joint return, wages use up that threshold first. On separate returns the investing spouse's income excludes the other's wages, and their gains start in their own 0% band. With about $200,000 of each, that saves $1,621. Every explainer gives the threshold. We found none that describes the split or where it pays.

Schedule 8812 pays more than the statute allows. This is a gap between the IRS form and the law, not a plan. The statute caps the refundable child credit per qualifying child, computed without the $500 credit for other dependents. The form caps the combined credit instead, so in the phase-out range, with no tax left to absorb it, it refunds the $500 credits in cash.[20],[21] Example: one child and one other dependent, $240,000 of income, no tax left. The statute gives $200, the form $700. Lean proves the form is never below the statute and agrees with it exactly when there are no other dependents.

6. Why one year of the tax code holds no big loopholes

The backdoor Roth is big because two provisions combine to remove an income limit entirely, and the money then compounds tax-free for decades. A single year of the individual income tax is full of cliffs and per-return thresholds, but each is bounded: the largest swin