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,<sup>[1]</sup> 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.<sup>[3]</sup> 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. Here we do that for one whole statute, the Internal Revenue Code, in three passes: check the text, model what it computes, and search what it permits.
1. The tax law’s text has 138 drafting mistakes #
The Office of the Law Revision Counsel publishes the US Code as structured XML.<sup>[4]</sup> We took release point 119-138, current to 3 November 2026, and turned Title 26 into data: every provision, down to the clause.
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](https://uscode.house.gov/us/usc/t26/s9818/#a-1-A) |
| Two provisions with the same number | 9 | [§1202(b)(4) appears twice](https://uscode.house.gov/us/usc/t26/s1202/#b-4)[§45X(d)(4) appears twice](https://uscode.house.gov/us/usc/t26/s45X/#d-4) |
| 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,<sup>[5]</sup> so each fault can be traced to the law that wrote it. For Title 26 the record reaches back to the 1994 edition.
Some faults do not show in the structure. §1401(b)(2)(B) reduces the self-employment threshold for the additional Medicare tax by wages “taken into account under section 3121(b)(2)”.<sup>[6]</sup> That section exists, so the reference resolves, but it covers domestic service by students in college clubs and imposes no tax. The section meant is §3101(b)(2), which is how Form 8959 applies it. The wrong number has stood since the Affordable Care Act.
2. Rewriting the income tax as code that can be checked #
To model what the law computes, we were inspired by the CPython project’s loop.<sup>[7]</sup> AI agents wrote each provision in Lean in the statute’s own words, tested it against printed IRS figures and examples (the Tax Table, the EIC table, the worksheets and publications), and proved properties of it. A fresh agent that had not written it then looked for errors. We did this in four groups: income and AGI (adjusted gross income: total income less a few items such as IRA contributions and student-loan interest, the figure most tax rules key off), deductions, the tax and the AMT (the alternative minimum tax, a second calculation that stops high earners from cutting their tax too far with deductions), and credits, all for 2025 as amended by the One Big Beautiful Bill Act.<sup>[8],[9]</sup> The reviewers found and fixed two real errors, in an AMT capital-gain band and in who may claim the premium tax credit, and withdrew one finding as a misreading.
Writing the model turned up five things:
- The official text is not the 2025 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.
- One Act, two rounding rules. The new tips and overtime deductions shrink by “$100 for each $1,000”, which rounds down. The new car-loan deduction phases out smoothly. So one more dollar of income can cost $100 of deduction, and the car deduction ends $999 before its stated range.
- The SALT phase-down treats separate filers harshly. They lose 15 cents of cap per dollar until it reaches $5,000 at $350,000. A couple at $300,000 each gets $25,000 from two separate returns against $10,000 from one joint return.
- The Tax Table is not the rate schedule. It differs by −$5 to +$6, proved for every income under $100,000 and every filing status.
- One dollar can cost $8,046. The EITC’s investment-income limit at $11,950 is a cliff, and the saver’s credit tiers are cliffs: a couple at $47,500 gets $2,000, at $47,501 they get $800.
3. Testing it against tax software people already use #
To check the model, we assembled the four groups into a Form 1040 and ran 5,000 households through it and through three tools built independently of each other and of us: PolicyEngine-US, the open model used in US policy analysis; Tax-Calculator, the Policy Simulation Library’s model; and UsTaxes, an open-source filing app.<sup>[10],[11],[12]</sup> Two thousand households were ordinary. Three thousand were hard cases: separate returns, surviving spouses, students, tips, overtime, IRAs, HSAs, education and saver’s credits, and seven-figure incomes with large gains.
Lean and PolicyEngine disagree on 7 households in 5,000, by at most $11. In all seven, Lean reads the IRS’s published EIC table and PolicyEngine applies the formula.<sup>[13]</sup> On every other quantity, for every household, they agree.
Tax-Calculator allows the EITC and the dependent-care credit on separate returns without the condition that the spouses lived apart, and computes no AMT for one high-income separate filer where the other two compute $14,881. UsTaxes has 14 bugs, each confirmed by recomputing a household. It silently drops self-employment income, because the 2025 return never attaches Schedule C. The dependent-care credit never reaches the return. The EITC age test is a stub that always returns true. Self-employment tax counts the spouse’s wages against the Social Security wage base. Together these bugs affect about one ordinary household in six.
The comparison also corrected our model twice. We had not counted Schedule C profit as qualified business income. And we always took the larger deduction, although §63(e) lets a taxpayer elect to itemize a smaller amount, which pays when it cuts the AMT. One household owed $2,070 less once that was in. Both errors surfaced because two independent tools agreed against 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:
| What the search found | Best case | Already described by |
|---|---|---|
| A business owner files separately to get under the §199A threshold | $6,317 a year | Kitces <sup>[\[14\]](#ref-14)</sup> |
| The lower earner claims the children on a separate return | $3,090 a year | practitioner guides <sup>[\[15\]](#ref-15)</sup> |
| Realize less gain to stay under the EITC investment limit | $6,798 for $5,000 deferred | IRS Publication 596 <sup>[\[13\]](#ref-13)</sup> |
| Itemize a smaller amount to cut the AMT | $2,070 a year | Form 1040 instructions | | Roth conversions in the gap years before Social Security | +$0.84M over a lifetime | Kitces |
| Pay your children wages, and open Roth IRAs for them | +$0.46M | Kitces <sup>[\[16\]](#ref-16)</sup> |
| Convert so the heirs do not stack ten-year withdrawals | +$0.43M–0.57M | Journal of Accountancy <sup>[\[17\]](#ref-17)</sup> |
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. Loopholes we could not find written down anywhere #
Three results did not turn up in practitioner sources, IRS guidance or tax-software forums. That is weaker than proof that they are new, so read them as “not found” rather than “new”.
Filing separately can cut tax on Social Security, even living together. The standard advice is that a couple living together should never file separately when one draws Social Security.<sup>[18]</sup> 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,<sup>[19],[20]</sup> 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.<sup>[21]</sup> 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.<sup>[22],[23]</sup> 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 none of them is large #
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 swing we found was a few thousand dollars. Over decades, the large gains come from moves that are already published. The one combination we could not find written up was paying the children in the same years as Roth conversions, which adds about 0.5%. Our guess is that anything Roth-sized and unpublished lives where value moves between entities and their owners: partnerships, S corporations and C corporations. That search is running now.
7. Most of this can now run automatically #
“The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. Some approaches aren’t really automatable, because they require a lot of both human and AI agent work.”
Taking the three layers in turn:
- The text checks are routine. A new release is one download and one command, which fails on any fault the last release did not have, and git blame names the Act responsible.
- The model is a one-off cost. Once written and proved, it is a build: if a later change breaks a proved property, the build fails. When the law changes, only the changed provisions go back through the loop.
- The comparison is routine once the input mappings are right. Getting them right was the hard part, and the same comparison found every mapping error.
What stays human is deciding what a finding means. Some cliffs are deliberate design, some faults belong to the forms rather than the statute, and some are artefacts of how the official text is put together.
Limits #
- Coverage. The model covers the 2025 individual income tax for a household record. It leaves out the kiddie tax on the single-year return, 28% and §1250 gain, foreign income, passive activity rules, and most AMT preferences. The multi-year model holds 2025 law constant.
- Who checked what. The drafting triage and the reviews were done by AI agents against the official text, and have not been checked by a lawyer.
- Agreement is not truth. Where all four calculators agree they may share a misreading. The theorems and the IRS-example tests are the check on the model itself.
The code, the certificates, the comparison and the searches are in the lean-proofs folder of global-law.[3]
References #
- Alan Yahya, ‘The auto-formalization of mathematics versus law’ (Lexifina , 7 September 2026)<lexifina.com/blog/auto-formalisation-of-law>
- Alan Yahya, ‘LEAN proof to search for US tax loopholes’ (Lexifina , 9 November 2026)<lexifina.com/blog/searching-the-tax-code-for-loopholes>
3. Lexifina, *global-law* , lean-proofs[<github.com/lexifina/global-law/tree/main/lean-proofs>](https://github.com/lexifina/global-law/tree/main/lean-proofs)
4. Office of the Law Revision Counsel, ‘United States Code: download’ (release point 119-138) [<uscode.house.gov/download/download.shtml>](https://uscode.house.gov/download/download.shtml)
5. Alan Yahya, ‘Git for the US Code’ (*Lexifina* )[<lexifina.com/blog/git-for-the-us-code>](https://lexifina.com/blog/git-for-the-us-code)
6. 26 USC § 1401(b)(2)(B) [<www.law.cornell.edu/uscode/text/26/1401>](https://www.law.cornell.edu/uscode/text/26/1401)
7. ‘Formalizing Python’ (*broyojo.com* )[<broyojo.com/python-formalization/>](https://broyojo.com/python-formalization/)
8. Internal Revenue Service, Rev Proc 2024-40 [<www.irs.gov/pub/irs-drop/rp-24-40.pdf>](https://www.irs.gov/pub/irs-drop/rp-24-40.pdf)
- An Act to provide for reconciliation pursuant to title II of H. Con. Res. 14, Pub L 119-21 (4 July 2025) <www.congress.gov/bill/119th-congress/house-bill/1>
10. PolicyEngine, *policyengine-us* (version 2.116.9)[<github.com/PolicyEngine/policyengine-us>](https://github.com/PolicyEngine/policyengine-us)
11. Policy Simulation Library, *Tax-Calculator* (version 6.8.5)[<github.com/PSLmodels/Tax-Calculator>](https://github.com/PSLmodels/Tax-Calculator)
12. *UsTaxes* (commit 49cd0f2, 7 November 2026)[<github.com/ustaxes/UsTaxes>](https://github.com/ustaxes/UsTaxes)
13. Internal Revenue Service, Publication 596, ‘Earned Income Credit’ (2025) [<www.irs.gov/publications/p596>](https://www.irs.gov/publications/p596)
- ‘Section 199A QBI deduction strategies for small business owners’ (Kitces.com )<www.kitces.com/blog/small-business-owner-section-199a-qualified-business-income-qbi-deduction-strategies/>
- ‘Child tax credit for married filing separately’ (Taxstra )<taxstra.com/child-tax-credit-married-filing-separately/>
- ‘Tax rules for hiring children in a family business’ (Kitces.com )<www.kitces.com/blog/tax-rules-hiring-children-family-business-flsa-tax-savings-standard-deduction-roth-contribution/>
- ‘Avoiding a big tax bill on inherited IRAs’ (Journal of Accountancy , May 2026)<www.journalofaccountancy.com/issues/2026/may/avoiding-a-big-tax-bill-on-inherited-iras/>
- ‘Should my wife and I file separate tax returns to avoid paying income taxes on her benefits?’ (Maximize My Social Security )<www.maximizemysocialsecurity.com/ask-larry/should-my-wife-and-i-file-separate-tax-returns-avoid-paying-income-taxes-her-benefits>
- Congressional Research Service, ‘Social Security: Calculation and History of Taxing Benefits’ (RL32552) <www.everycrsreport.com/files/20150120_RL32552_fa08c40941ceb4e9565c7c7cbd9a4e8e8ba46cdc.html>
- Congressional Research Service, ‘Taxation of Social Security Benefits and the Senior Deduction in P.L. 119-21: In Brief’ (R48613) <www.everycrsreport.com/reports/R48613.html>
21. 26 USC § 1411 [<www.law.cornell.edu/uscode/text/26/1411>](https://www.law.cornell.edu/uscode/text/26/1411)
22. 26 USC § 24(d), (h)(4)–(5) [<www.law.cornell.edu/uscode/text/26/24>](https://www.law.cornell.edu/uscode/text/26/24)
23. Internal Revenue Service, Schedule 8812 (Form 1040) (2025) [<www.irs.gov/forms-pubs/about-schedule-8812-form-1040>](https://www.irs.gov/forms-pubs/about-schedule-8812-form-1040)