Lean proof to search for US tax loopholes

A Lean model of US retirement-account rules demonstrates how formal search can uncover interactions among provisions rather than relying on experts to anticipate them. The example is the backdoor Roth: although high earners cannot contribute directly to a Roth IRA, they can contribute after-tax money to a traditional IRA and convert it. The pro-rata rule normally makes a conversion partly taxable when the saver has other pre-tax IRA assets, but rolling those assets into an employer 401(k) can leave after-tax IRA money available for a tax-free conversion. A second route, the mega backdoor Roth, moves after-tax 401(k) contributions into the plan’s Roth account.

The model represents five account types and seven permitted transactions, then searches possible sequences for a high-earning taxpayer with $100,000 in a rollover IRA and $100,000 in savings. Among 345,075 positions explored to six moves, it finds a tax-free $77,000 Roth contribution: $70,000 through the mega backdoor and $7,000 through the IRA route. Formal proofs establish broader results than the search alone, including that the IRA contribution route works above the income limit and that $77,000 is the annual ceiling within the model. The authors stress that this is a simplified demonstration, not tax advice: it omits factors such as employer-plan eligibility and applies the pro-rata rule differently from the Code’s year-end calculation. Its larger promise is testing proposed laws and finding unanticipated workarounds.