Lean proof to search for US tax loopholes

A team behind the CC0-licensed global-law repository of versioned legislation and caselaw encoded a corner of the US Internal Revenue Code in Lean and ran an automated search over every permitted sequence of seven account moves, with a theorem prover checking the results, to test whether AI pointed at a versioned legal record can surface contradictions and loopholes. The model used 2025 limits — including the $150,000–$165,000 modified adjusted gross income phase-out for single-filer Roth IRA contributions and the $70,000 overall 401(k) additions limit — and started from a single filer earning $250,000 with $100,000 in pre-tax IRA savings. The search reproduced the known backdoor Roth route, in which a non-deductible traditional IRA contribution is converted the next day, and the mega backdoor route through after-tax 401(k) contributions, on a provision set where the answer was already known so the method could be judged.

Lean proof to search for US tax loopholes Navier stokes? That will never make money. Instead, we compiled a Lean proof to find loopholes in the US tax code. But first, a step back. This example is part of the vulnerability monitoring work we do at global law https://github.com/lexifina/global-law , a CC0 repo of versioned legislation and caselaw. Our argument is that we can point AI at a versioned record of the law to find contradictions and other key logical mistakes in our system of legislation and interpretation. Loopholes are usually found by someone who knows two provisions well and sees that together they allow what neither allows alone. That depends on who is looking, and nobody can say whether their route is the best one. We wrote the rules down with no strategy built in, let a search try every sequence of moves they permit, and had a theorem prover check the result, on a corner of the Internal Revenue Code where the answer is already known, so that the method could be judged. The routes around the rules A Roth IRA is taxed at the front and never again, which makes it valuable to people with a long time to save. Congress limits who may contribute to one. The amount a single filer may put in shrinks between $150,000 and $165,000 of modified adjusted gross income and is zero above that.<sup \ 1\ ref-1 , \ 2\ ref-2 , \ 3\ ref-3 </sup Since 2010, though, there has been no income limit on converting a traditional IRA into a Roth IRA, and anyone may make a non-deductible contribution to a traditional IRA whatever they earn.<sup \ 4\ ref-4 , \ 5\ ref-5 , \ 6\ ref-6 </sup Put those two together and the income limit stops nobody: contribute to a traditional IRA, convert it the next day, and the money is in a Roth. Practitioners call this the backdoor Roth. It is widely treated as a loophole: the House voted to close it in 2021,<sup \ 7\ ref-7 , \ 8\ ref-8 </sup and the chair of the Senate Finance Committee was reported the same year to be preparing a crackdown on Roth accounts used by the wealthiest savers. \ 9\ ref-9 There is a catch, and then a way round the catch. When money comes out of a traditional IRA, all of a person's IRAs are treated as one account, and each dollar converted is deemed to be the same mix of taxed and untaxed money as the whole.<sup \ 6\ ref-6 </sup Someone with $100,000 of pre-tax savings in an old IRA who adds $7,000 of after-tax money and converts $7,000 is taxed on most of it. But money rolled from an IRA into an employer's 401 k plan can only be the pre-tax part, and is treated as coming from that part first.<sup \ 6\ ref-6 </sup Move the old savings into the 401 k and what is left in the IRA is all after-tax, so the conversion costs nothing. A separate route runs through the 401 k itself: the plan can accept after-tax contributions up to the overall limit on additions, $70,000 in 2025, and move them into its own Roth account, the route known as the mega backdoor. \ 10\ ref-10 , \ 11\ ref-11 , \ 8\ ref-8 Writing the rules down We wrote these provisions in Lean, a programming language whose type checker can also check mathematical proofs. An earlier post discussed how far that kind of formalisation can reach in law.<sup \ 12\ ref-12 </sup Here the model is small. A taxpayer has five accounts: cash, the traditional IRAs taken together, the Roth accounts, and the pre-tax and after-tax parts of a 401 k . There are seven moves between them, each written from the provision that governs it, with the 2025 limits: contribute to a Roth IRA, contribute to a traditional IRA, convert, roll IRA money into the 401 k , defer salary, make an after-tax 401 k contribution, and roll that into the plan's Roth account. A move either is allowed, with its effect on each balance and on taxable income, or is not. What the search found The search starts from one person: a single filer earning $250,000, so far above the Roth limit, with $100,000 of pre-tax money in a rollover IRA from an old job and $100,000 in savings. It tries every move with every amount the position naturally offers what is left of each limit, each balance, the pre-tax part, the after-tax part and keeps going, breadth first, to six moves deep. That is 345,075 distinct positions. It is asked one question: how much can go into Roth accounts without any tax? The answer is $77,000, in five moves. Contribute $70,000 after tax to the 401 k and roll it into the plan's Roth account; contribute $7,000 to a traditional IRA; roll the $100,000 of pre-tax IRA money into the 401 k ; convert the $7,000. Both the backdoor and what practitioners call the mega backdoor come out of the search without having been described to it, and so does the order the backdoor needs. Forbidden the roll-in, the cheapest way to get the same $7,000 into the Roth is to contribute and convert, with $6,543 of it taxed. Run again for the same person earning $140,000, the search simply makes a Roth contribution. What the proofs add A search only reports what it saw, and it stopped at six moves. The proofs cover every sequence of moves of any length, from any starting position, and Lean accepts none of them until every step checks. There are four. The first is a conservation law: pre-tax money leaves the IRAs only by being taxed or by being rolled into the 401 k . From it follows the second, that without the roll-in every pre-tax dollar is taxed on its way to the Roth, however the conversions are split, ordered or repeated. The step that needed most care was rounding. The statute's proportion has to be computed in whole dollars, and Lean's automatic arithmetic could not show that rounding never taxes more than the pre-tax money there is, so that inequality was proved by hand. The third is that for every income above the limits, and every starting set of accounts, there is a permitted sequence that puts $7,000 into a Roth with no tax. That is exactly what the income limit in section 408A is meant to prevent. The fourth is a ceiling: in a year, no plan puts more than $77,000 of new money into Roth accounts at no tax, plus whatever after-tax money was already held. Since the search found a plan that reaches the ceiling, its plan is proved to be the best one in the model. In simplified form: theorem roth ceiling income : Nat moves : List Move : ∀ before after, run income before moves = some after → after.roth − before.roth ≤ 7000 + 70000 + before.iraBasis + before.planAfterTax + after.taxed − before.taxed Limits The model applies the pro-rata rule at the moment of each conversion. The Code uses the value of all IRAs at the end of the year,<sup \ 13\ ref-13 </sup which is more forgiving about order: a conversion made before the roll-in, in the same year, is also tax-free. The plan the search found works on either reading, but other orderings would come out differently, and the next version should use the year-end rule. Whether a person can use the second route depends on their employer's plan, and after-tax contributions by higher-paid employees are often cut back by the nondiscrimination test in section 401 m .<sup \ 14\ ref-14 </sup The model knows nothing about state tax, employer contributions or investment growth. And a proof says only that the result follows from the rules as written in the model. Each rule was checked against the statute by hand, and that check is the part a reader should question. Why it matters None of this is news to a tax adviser, which is why it was chosen. Congress has looked at these routes too. The version of the Build Back Better Act passed by the House in November 2021 would have barred converting after-tax money from 2022 and so closed both.<sup \ 7\ ref-7 , \ 8\ ref-8 </sup The bill stalled in the Senate, and the Inflation Reduction Act that replaced it in 2022 left the provision out.<sup \ 15\ ref-15 </sup Nothing enacted since has revived it, and both routes remain available in 2026.<sup \ 16\ ref-16 </sup What is new is that the routes and their limits fall out of the rules mechanically, together with a proof that nothing in the model does better. The more interesting places to point this are those where no one has catalogued the interactions: provisions that were amended at different times, or a bill before it passes. A drafter could write the proposed change into the same model and ask the search whether the limit they are adding can be walked around, and the proofs would say whether a fix closes every route or only the one someone thought of. It is the same idea as our search for drafting mistakes in published law https://lexifina.com/blog/mass-zero-day-vulnerability-detection-in-legal-code , applied to what the law permits rather than how it was written. The model and the search are public in global-law; see the lean-proofs https://github.com/lexifina/global-law/tree/main/lean-proofs folder. Isn't a lot of this deliberate? Law is grey on purpose. Often, yes. The detectors look for mechanical mistakes, not grey areas: a reference to a section that was repealed or renumbered, a fine that points at a deleted rule, a rule in force before it was published. Whether a gap is a mistake or a choice is a legal judgement, so every review gives a verdict, and most flags turn out to be lawful, cured, intended or errors in a corpus rather than defects in the law. The law isn't software. Why apply software-style checks? It isn't, and these checks do not try to prove a statute correct. They work like a linter: they catch the mechanical slips references that point nowhere, impossible dates, amendments that could not be carried out that drafters would fix if they saw them. Who benefits, and will legislators ever adopt this? It needs no one's adoption: published law is public, so anyone can run the checks. Finding these mistakes used to take legal training and time; publishing them puts pressure on legislatures to repair them, and lets everyone, not only well-advised insiders, see where the text fails. References 1. 26 USC § 408A c 3 <www.law.cornell.edu/uscode/text/26/408A https://www.law.cornell.edu/uscode/text/26/408A 2. Internal Revenue Service, Notice 2024-80, ‘2025 Limitations Adjusted as Provided in Section 415 d , etc.’ 1 November 2024 <www.irs.gov/pub/irs-drop/n-24-80.pdf https://www.irs.gov/pub/irs-drop/n-24-80.pdf 3. Internal Revenue Service, Publication 590-A, ‘Contributions to Individual Retirement Arrangements IRAs ’ <www.irs.gov/pub/irs-pdf/p590a.pdf https://www.irs.gov/pub/irs-pdf/p590a.pdf 4. Tax Increase Prevention and Reconciliation Act of 2005, Pub L 109-222, s 512 <www.congress.gov/109/plaws/publ222/PLAW-109publ222.pdf https://www.congress.gov/109/plaws/publ222/PLAW-109publ222.pdf 5. ‘Roth IRA Conversions in 2010’ The Tax Adviser , October 2009 <www.thetaxadviser.com/issues/2009/oct/rothiraconversionsin2010/ https://www.thetaxadviser.com/issues/2009/oct/rothiraconversionsin2010/ 6. 26 USC § 408 d 2 , d 3 A ii , d 3 H and o <www.law.cornell.edu/uscode/text/26/408 https://www.law.cornell.edu/uscode/text/26/408 7. Build Back Better Act, HR 5376, 117th Congress as passed by the House of Representatives, 19 November 2021 <www.congress.gov/bill/117th-congress/house-bill/5376 https://www.congress.gov/bill/117th-congress/house-bill/5376 8. ‘Build Back Better Act would curb retirement plans for the wealthy’ CNBC , 19 November 2021 <www.cnbc.com/2021/11/19/house-passes-build-back-better-act-retirement-plans-for-the-wealthy.html https://www.cnbc.com/2021/11/19/house-passes-build-back-better-act-retirement-plans-for-the-wealthy.html 9. ‘The Ultrawealthy Have Hijacked Roth IRAs. The Senate Finance Chair Is Eyeing a Crackdown.’ ProPublica , 2021 <www.propublica.org/article/the-ultrawealthy-have-hijacked-roth-iras-the-senate-finance-chair-is-eyeing-a-crackdown https://www.propublica.org/article/the-ultrawealthy-have-hijacked-roth-iras-the-senate-finance-chair-is-eyeing-a-crackdown 10. 26 USC §§ 402 g , 402A c 4 and 415 c <www.law.cornell.edu/uscode/text/26/402A https://www.law.cornell.edu/uscode/text/26/402A 11. Internal Revenue Service, ‘COLA increases for dollar limitations on benefits and contributions’ <www.irs.gov/retirement-plans/cola-increases-for-dollar-limitations-on-benefits-and-contributions https://www.irs.gov/retirement-plans/cola-increases-for-dollar-limitations-on-benefits-and-contributions 12. Alan Yahya, ‘The auto-formalization of mathematics versus law’ Lexifina , 7 September 2026 <lexifina.com/blog/auto-formalisation-of-law https://lexifina.com/blog/auto-formalisation-of-law 13. Internal Revenue Service, ‘Instructions for Form 8606: Nondeductible IRAs’ <www.irs.gov/instructions/i8606 https://www.irs.gov/instructions/i8606 14. 26 USC § 401 m <www.law.cornell.edu/uscode/text/26/401 https://www.law.cornell.edu/uscode/text/26/401 15. ‘Backdoor Roth 401 k and IRA rules for the wealthy survive — for now’ CNBC , 20 December 2021 <www.cnbc.com/2021/12/20/backdoor-roth-401k-and-ira-rules-for-the-wealthy-survive-for-now.html https://www.cnbc.com/2021/12/20/backdoor-roth-401k-and-ira-rules-for-the-wealthy-survive-for-now.html 16. ‘Making a backdoor or mega backdoor Roth contribution in 2026’ Mercer Advisors , 2026 <www.merceradvisors.com/retirement/making-a-backdoor-or-mega-backdoor-roth-contribution-in-2026/ https://www.merceradvisors.com/retirement/making-a-backdoor-or-mega-backdoor-roth-contribution-in-2026/