Wow, if I'm reading this correctly, the Big Beautiful Bill introduced a pretty large gap that punishes married couples filing jointly: a couple making about $300K each can lose up to $15K in write-offs compared with filing separately, pretty much everywhere except the nine states with no broad income tax (Alaska, Florida, Nevada, New Hampshire, South Dakota, Tennessee, Texas, Washington, and Wyoming), where few couples pay the $25K in state and local taxes needed to trigger it. I think most tax software will assume the $5K cap each, but the regulation here is inconsistent. Here’s the take-away quote from the article:
“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.”
This is non-trivial impact to joint returns if this is true, and I won’t be surprised if there are multiple appeals for refunds and more people filling separately going towards.
> punishes married couples filing jointly: a couple making about $300K each
The number of married couples where each partner is making $300K each is a very, very small percentage of the population. Not sure this is a big deal to be concerned about in the grand scheme of things. For instance, only a few %age of households have an income over 300K in the first place, much less coming from 2 earners of that amount.
It’s a neat idea but I don’t understand what value Lean adds here. Is there really anything to “prove” in the tax code? Or are they just using Lean as a scripting language?
Yes, the tax code is basically "if this condition and that condition then pay $". So if they can find a condition that isn't covered, they can theoretically pay less tax. There is an XKCD of course: https://xkcd.com/1494.
I assume you'd want to prove common-sense invariants, like "you can't be taxed more than your income" or "tax credit 123-45 is worth more for two children than for one". Lean might disprove a few of these, and the counterexamples are potential loopholes.
i love that people are trying to do this and democratizing access to the code. one day i hope to have the power of a compentent CPA just an API call away. Until then I trust my highly paid CPA.
Wow, if I'm reading this correctly, the Big Beautiful Bill introduced a pretty large gap that punishes married couples filing jointly: a couple making about $300K each can lose up to $15K in write-offs compared with filing separately, pretty much everywhere except the nine states with no broad income tax (Alaska, Florida, Nevada, New Hampshire, South Dakota, Tennessee, Texas, Washington, and Wyoming), where few couples pay the $25K in state and local taxes needed to trigger it. I think most tax software will assume the $5K cap each, but the regulation here is inconsistent. Here’s the take-away quote from the article:
“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.”
This is non-trivial impact to joint returns if this is true, and I won’t be surprised if there are multiple appeals for refunds and more people filling separately going towards.
> punishes married couples filing jointly: a couple making about $300K each
The number of married couples where each partner is making $300K each is a very, very small percentage of the population. Not sure this is a big deal to be concerned about in the grand scheme of things. For instance, only a few %age of households have an income over 300K in the first place, much less coming from 2 earners of that amount.
It’s a neat idea but I don’t understand what value Lean adds here. Is there really anything to “prove” in the tax code? Or are they just using Lean as a scripting language?
Maybe tax change impact analysis by congress can easily be calculated using Lean. The article also said loopholes can be easily identified?
Yes, the tax code is basically "if this condition and that condition then pay $". So if they can find a condition that isn't covered, they can theoretically pay less tax. There is an XKCD of course: https://xkcd.com/1494.
I assume you'd want to prove common-sense invariants, like "you can't be taxed more than your income" or "tax credit 123-45 is worth more for two children than for one". Lean might disprove a few of these, and the counterexamples are potential loopholes.
this is actually a really bad idea and is the opposite of what a powerful state would want
maybe some rationale? states should want to preclude people from reasoning about tax laws?
i love that people are trying to do this and democratizing access to the code. one day i hope to have the power of a compentent CPA just an API call away. Until then I trust my highly paid CPA.