I worked for a company pre-LLMs that analyzed laws and regulations in order to answer questions about financial transaction legality and reporting requirements. One problem that came up frequently is that the rules governments make don't have to be consistent. There are conflicts, some quite significant. The best we could do was make them visible and escalate to a human.
It would be interesting to require laws to be compilable. Charles Stross wrote a couple of books that include that idea.
In theory "impossibility" is a defense to most crimes.
In practice you usually get screwed in one of the following ways: a) the law makes it impossible to do X without breaking the law, even though X is a normal thing and neither law was supposed to be a total ban on X, but you could comply by not doing X at all, b) the inconsistent laws are imposed by different jurisdictions and then they each insist you follow theirs, often a special case of the first one where X is "be in two different jurisdictions" but sometimes the even stupider one where a jurisdiction demands that you follow its laws even when you're not in it, c) it's impossible for you to follow both laws at once so you followed only one of them and then they decide after the fact that you should have followed only the other one.
Re: imposed by different jurisdictions. I don't know the letter of the law in the US, but here in Australia at least, most such differences are easily resolved by section 109 of our constitution (note: Commonwealth == Federal):
"When a law of a State is inconsistent with a law of the Commonwealth, the latter shall prevail, and the former shall, to the extent of the inconsistency, be invalid."
Hmmm, just googled, and it would seem that Article VI Clause 2 of the US constitution, aka the Supremacy Clause, is basically equivalent.
In the US, the Supremacy Clause only holds insofar as federal law doesn't overstep the restrictions on federal power outlined elsewhere in the Constitution. The wording is "the Laws of the United States which shall be made in Pursuance [of the Constitution]".
If you follow federal law over state law, but then a federal judge holds that the federal law you followed was an unconstitutional overstep in a domain that the Constitution reserves to the states, you are SOL
This might be happening with the founders of Kalshi. The federal law and CFTC has been saying that these prediction markets are federally regulated, but they're facing criminal charges in some states.
Kalshi isn't "bets", it's a "market" where people trade contracts related to the outcome of the sports game. I think that's the argued legal distinction.
I think it's nonsense and that gambling is very destructive, but there does seem to be a line there where sometimes sports betting is betting, and other times it's trading in a market.
You're assuming the contradiction is between a federal law and a state law and not e.g. a law of the US and a law of France.
One of the more recent fun absurdities is some jurisdictions claiming that if you have a service accessible over the internet then you're subject to their (i.e. every) jurisdiction.
Suppose you have a law that says that in order to build new multi-unit housing, a given percentage of the new units have to be affordable housing and have to be built within reasonable distance of a transit stop in the same town. Meanwhile you have a town with poor mass transit and very little land zoned for multi-unit housing, and none of it overlaps. In other words, you're both required to and prohibited from building new affordable housing units near a transit stop. Which means you also can't build the other units.
Which law are you breaking if you build no housing whatsoever?
Notice that there are many cases of this where that kind of outcome is what you want, e.g. if there is a law against operating e-bikes above 20 MPH and a law against going below 40 MPH on the freeway and the de facto result is "no e-bikes on the freeway" then that's a pretty reasonable outcome.
Whereas "no new housing" is a presumably unintended absurdity, but that doesn't mean you're guaranteed a way out of it.
There are also many cases where rather than being required to do something impossible you're required to do something infeasible, which in practice is the same thing but then they get to point to the entire mountain of shit you'd be required to eat and suggest that you do that.
Accelerando was the one I was thinking of. I believe he has some other short stories with Manfred Macx, but I'm not finding them on my shelf immediately.
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.
I just think the team did a good job from what I’m reading. This inconsistency doesn’t impact the top 1% household (who commonly use larger loopholes to avoid taxation at magnitudes more significant than this inconsistency like using loan against assets which they can write off interest against taxes instead of paying taxes to the government). This quirk impacts households in the 2% level for just one fiscal year or more where they might just have a taxed event like a real estate sale (non reinvested primary within the timeline), a taxable equity grant (that the pay taxes on but may lose), one time capital gains from investment sales, etc.
Tax law is supposed to be consistent and fair in general, and the introduction of the Big Beautiful Bill created a weird quirk here, that gets quirkier that you can file separately and correct to jointly but not the other way around legally right now. From 2018–2024, the tax code was consistent on SALT, then in 2025 and looking forward to 2029 SALT taxation becomes inconsistent under certain joint filing conditions that impact a non-trivial number of households especially when it starts at $250k each, or a lopsided earnings of that combined amount and peaks at the $600k.
This team is identifying a pretty big quirk that goes against the principle of consistency in tax law and did a very good job of it applying formal logic to law if they prove this to be correct. Others have done too before AI (which is what your tax software is conservatively doing), but it’s just easier now with AI.
> I just think the team did a good job from what I’m reading. This inconsistency doesn’t impact the top 1% household (who commonly use larger loopholes to avoid taxation at magnitudes more significant than this inconsistency like using loan against assets which they can write off interest against taxes instead of paying taxes to the government). This quirk impacts households in the 2% level for just one fiscal year or more where they might just have a taxed event like a real estate sale (non reinvested primary within the timeline), a taxable equity grant (that the pay taxes on but may lose), one time capital gains from investment sales, etc.
The top 1% have a significant portion of high-income W2 earners who basically have been forced into the standard deduction since the TCJA. It definitely impacts them because that's exactly what the SALT cap was designed to do.
The business owners (lawyers, dentists, investment bankers) are the ones that have all the fun tax breaks, and they're probably more like top-0.1%.
It might be a few people nationwide, but it's a whole lot of families in the Bay Area, New York, Los Angeles, and a few other major cities.
The law was specifically designed to punish these people. Remember, at first they wanted to drop the SALT deduction completely to punish blue states.
Edit: It seems that people are assuming I'm against removing the SALT deduction. Far from it. I am glad they got it done despite being a political third rail for a long time. And despite being a huge beneficiary of the SALT deductions myself.
I don't think people choosing to live in high tax states should get to save on their federal income taxes.
A family making $300k in Manhattan should not be taxed a lot, unless you think a family making ~$115k in Montgomery, Alabama should also be taxed a lot.
Policy is best written by the informed rather than the emotional.
I live in a borderline HCOL/VHCOL city, and arguments like this get thrown around a lot on local boards. But yet the median household income is right around 100k.
People on sites like this tend to have a skewed view of normal.
Also we're discussing a household income of 600k+, not 300k.
Livable income = income that pays for (housing, food, clothing, transportation, medical preventative care and treatment, an emergency fund) x 4
( x 2 for retirement savings without assumption of unbounded economic growth, x 2 for government stealing half your money [1])
I don't think the median is making that number. So that's not the number I'd go off of.
[1] pre-emptive note to shut up the people who will inevitably come to this forum just to lecture me that taxes aren't that high. they are. a LOT of government money-stealing is hidden into things that aren't paid in April, and things that aren't explicitly labelled as taxes.
If you're going to claim that literally half the households living in a city aren't making a livable wage, then I'm going to claim you're exactly the type of person I'm describing who has a cushier view of livable wage than reality.
I agree that your definition is a comfortable living, but that's not reality for the majority of americans.
I assure you that a married couple making 600k a year has plenty of money.
Also, the government stealing half of your money is a ridiculous over-exaggeration. This year my MFJ household income will be around $950,000. My effective tax rate is nowhere near 50%.
No, you should be taxed a lot. [edit: you just said "those people should be taxed a lot" with no reason and then people get sad when the same is said to them]
Don’t tax the rich (and yes, 600k for a couple per year is absolutely rich territory)? “They need to pay their fair share!” Tax the rich? “They’re targeting people in blue cities!”
The SALT deduction is nonsense. Why should high tax states effectively be able to take money from the federal government?
States should be encouraged to provide services to their citizens and reduce burden on federal programs, allowing SALT write offs is part of that. This should be a "win" for all the smaller fed government folks many states are not taxing at appropriate levels and then take a bunch of federal money.
It's funny that me pointing out the fact removing the SALT deduction was meant to punish rich people makes people think I don't like it.
In fact, I was glad they got it done. The Dems didn't object very hard because they knew it had to go too. It's interesting that they didn't put it back when they had the chance.
I don't think the federal government should lose money when people choose to live in high tax states. And I pay high taxes in a high tax state.
It’s even more nuanced than that. The no income tax states like Florida get supplemented more from the federal government. So fed taxes with SALT limits are relatively shifting even more burden to the residence of states who tax their residence and pay for their own local services, which then having to do pay more of the burden for no income tax states.
The tax code has significantly punished dual-income married couples for quite a while. It presumably started some time in the 20th century as some sexists not wanting women in the workplace and then continued because changing it to have them pay the same taxes as they would if they were unmarried would result in a significant reduction in government revenue.
> Today, we set out to formalize the entire Internal Revenue Code to hunt for unknown loopholes (bugs).
Saying that loopholes are bugs is a political statement that a particular allocation of resources is inherently fraudulent. There is no data that Lean code could use to decide whether a result is intentional or not.
It's like deciding that any tax provision that increases income inequality is illegitimate, and writing code to identify them. That could be a useful exercise, but it isn't a way to justify a human value with math. It may be a formalization of an ethic as applied to a tax code, but not of the tax code.
Any change to the law that bill authors have to hide by phrasing the bill so that it sounds like the change is otherwise is illegitimate, and that's what formalization is meant to catch.
I think there are more such loopholes than most people realize.
From The Blind Spot: How Oligarchs Dominate Our Democracy by Jeffrey Winters: "When it comes to winning advantages for wealthy and powerful clients, lobbyists focus in on micro-details no one else is paying attention to but which could mean millions or billions saved by clients. 'Sometimes we were changing a word and that's all that we needed,' one lobbyist admitted."
Agreed. In fact, you'll see things termed loopholes vs. benefits depending entirely on politics so it can't be a property of the law itself. An EV tax credit or SALT deduction are "loopholes" too.
It's important to remember that the loopholes are often intentional. They are left there so that rich people who can afford CPAs can take advantage of them, while middle income and poor people cannot afford to.
They are also left there so there is wiggle room for interpretation if it comes in front of an auditor or a judge.
And also, it's important to remember that in tax matters, the final arbiter of interpretation is a judge. Judges are humans, not machines. You can't "Trick" them by saying "well technically this is allowed!". Because they rule on the sprit of the law, not as it was written. Judges aren't amused when you try to be cute with how you interpret a law. And some Judges have biases, where you get a different ruling depending on if you play at their golf club or not.
Laws aren't computer code. They are vague on purpose.
I've heard this repeated a couple times here on HN. Do you have any citations for laws being vague on purpose? The whole point of laws, and the formal structure they take, is to reduce vagueness. Is this rock on person A's land or person B's land? When it turns out, despite best efforts, that a law is vague we even have a second system to step in and reduce the vagueness further: case law. I have no doubt that people are trying to exploit vagueness on both sides, but naysaying here is nonsense. And almost nobody wants law to be vague either.
Lawyer here (but I don't make any money from it and absolutely have no dog in this fight). I agree. Law is vague for two reasons - first it is often as a compromise between two positions that people were okay having decided on a case by case basis instead of fighting to the death over what to write down. It also is vague sometimes to intentionally capture the spirit of what it is trying to do. While I won't claim vagueness is never left to benefit someone ( I'm sure it happens), I would claim it is rare.
Law is basically a representation of societal judgement. While criminal law is intended to be clear enough to know when you've violated it, that is not the same as beimg logical or consistent. Civil law is even less logical and consistent. Formalizing it into logic generally does not make sense overall - it isn't really broken in most cases because it was never intended to be totally consistent. There are certainly areas that could use cleaner rewriting but courts are generally well equipped to figure out what it means. Congress and the states can always overturn interpretations of law, but the rate at which they rewrite laws because they thought courts interpreted it wrong is very, very low.
> And also, it's important to remember that in tax matters, the final arbiter of interpretation is a judge. Judges are humans, not machines. You can't "Trick" them by saying "well technically this is allowed!". Because they rule on the sprit of the law, not as it was written. Judges aren't amused when you try to be cute with how you interpret a law. And some Judges have biases, where you get a different ruling depending on if you play at their golf club or not.
> Laws aren't computer code. They are vague on purpose.
Yes... but. Tax law is a bit different because it is similar to an equation: you put in your inputs and you get your outputs.
There have been famous cases where the courts have said in essence, "yes you completely and exactly and precisely followed the law, but we're not going to allow you to do that anyway." Those rulings have become less frequent.
No it is not a flawed system. That is literally the legal system at work (at least the Westminster / US systems with judge-developed case law). Legislature writes the law, and nobody knows for sure what constitutes "complying with or being in breach of that law" until judiciary rules on it (sometimes decades later!).
This is ridiculous - first of all you don’t have to be rich to afford a CPA, second of all high earners almost always pay the highest rates (both effective and marginal). And even in the cases where they don’t pay huge marginal rates (dividends and LTCG), they don’t need a CPA to take advantage of that because it’s dead simple.
I'm not talking about a high earner who makes a few hundred thousand a year. I'm talking about the high earner who is making a few million a year and taking advantage of the vague tax laws by paying a CPA tens of thousands of dollars to do their returns for them and then save them a few hundred thousand in taxes.
And yes I'm aware that the wealthy pay most of the taxes. I'm fine with that. I'm just pointing out that these laws are made so they still pay less than they would otherwise.
It depends on how you are making these millions. A W-2 employee at meta making $1M or more per year is almost certainly paying over 50% marginal tax rates (combined state and federal). And there is virtually nothing you can do to lower that burden by any significant amount.
The tax code benefits certain types of income, but it does not uniformly benefit high earners, as you say.
> Because they rule on the sprit of the law, not as it was written.
I feel like this attitude is responsible for the modern destruction of the rule of law.
It doesn't matter what the law says, the only thing that matters is vibes! And whether you play golf with the right government officials.
> You can't "Trick" them by saying "well technically this is allowed!".
The obvious problem being that sometimes it is allowed. And then do you want that being decided by democratically elected representatives and specified ahead of time so the public can know what's expected of them and of others, or decided ex post facto on the basis of feels and discrimination?
> Because they rule on the sprit of the law, not as it was written.
Extremely funny to say that about US law when it is entirely based on precedent, and a single judge having vibes on a particular day changes how your entire country works for the next 50 years.
US law is explicitly made to be skirted, as is every common law system in the world and they are all irrevocably flawed.
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?
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.
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.
This is the case where the xkcd doesn't apply though.
The thing about insurance fraud is that the major thing that will cause it to be fraud is when you set the fire on purpose.
The tax code doesn't really have that. You'll often even see confused people inserting nonsense language in various places to the effect that doing something to avoid taxes isn't allowed, but meanwhile "doing something to avoid taxes" is the expected mechanism of operation for tax incentives meant to get people to do something they otherwise wouldn't have done.
And then because of that you need to actually care about what the tax code says and what the unnecessarily complicated nonsense allows someone to get away with without breaking the law, instead of pretending that it's all common sense and people can be punished for being "bad" without ever actually specifying what that means.
You wouldn’t be proving the tax code, you’re proving that a procedure follows the tax code. This way you’d be able to know for certain if an AI that tried reducing your taxes actually gives you a valid procedure/result, assuming you can trust the Lean formalization (hint: you can’t given the nature of law, especially if it’s vibe coded like this)
Maybe you could validate stuff, like "how much would I be taxed if I did X" and then have it come up with all the questions that need to be answered to determine the answer or "what's the max I could be taxed if I did Y"?
I don't know much about Lean, but I assume that beyond proving things it functions as a truth graph you could walk to calculate things...
Edit, it might also be (someday) useful when drafting tax law to make sure the law is actually sound (e.g. isn't contradicting something else) or to see what it's overlapping with?
"The comparison caught ... mistakes in our own model too. We had not counted self-employment profit toward the 20% deduction for small-business income"
This seems like a pretty big oversight? Makes it feel like there might be a lot more low-hanging fruit, much less subtitles to explore?
If the tax law is inconsistent (as some of the comments seem to indicate), does that mean that we don't have to pay any tax or even are entitled to a large tax credit? After all, Lean supports the principle of explosion (https://en.wikipedia.org/wiki/Principle_of_explosion).
interesting idea. the concept of formalizing legal code is attractive to me, if only because i am addicted to logic. but realistically this will be hard to extend past tax code. formalization of law is more difficult in common law, which is heavily driven by judicial presedent, which is fluid and resists codification. a machine learning algo trained on cases might perform better, but even then, so many cases cant be determined easily.
I've been reading a very sobering book that came out this year, The Blind Spot: How Oligarchs Dominate Our Democracy and what I've read tells me that for the people who are running things the loopholes are features and not bugs. I strongly recommend this book. Things like Nixon's sabotage of the IRS, the revolving door of employment in US Treasury and private tax law firms, the labyrinthine nesting of partnerships inside pass-through partnerships—it's shocking stuff.
this is actually wonderful. and a good use of the tech. ive been joking about wanting to do this for years, but the sheer magnitude of work made it impossible for me to consider doing
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.
I worked for a company pre-LLMs that analyzed laws and regulations in order to answer questions about financial transaction legality and reporting requirements. One problem that came up frequently is that the rules governments make don't have to be consistent. There are conflicts, some quite significant. The best we could do was make them visible and escalate to a human.
It would be interesting to require laws to be compilable. Charles Stross wrote a couple of books that include that idea.
In theory "impossibility" is a defense to most crimes.
In practice you usually get screwed in one of the following ways: a) the law makes it impossible to do X without breaking the law, even though X is a normal thing and neither law was supposed to be a total ban on X, but you could comply by not doing X at all, b) the inconsistent laws are imposed by different jurisdictions and then they each insist you follow theirs, often a special case of the first one where X is "be in two different jurisdictions" but sometimes the even stupider one where a jurisdiction demands that you follow its laws even when you're not in it, c) it's impossible for you to follow both laws at once so you followed only one of them and then they decide after the fact that you should have followed only the other one.
Re: imposed by different jurisdictions. I don't know the letter of the law in the US, but here in Australia at least, most such differences are easily resolved by section 109 of our constitution (note: Commonwealth == Federal):
"When a law of a State is inconsistent with a law of the Commonwealth, the latter shall prevail, and the former shall, to the extent of the inconsistency, be invalid."
Hmmm, just googled, and it would seem that Article VI Clause 2 of the US constitution, aka the Supremacy Clause, is basically equivalent.
In the US, the Supremacy Clause only holds insofar as federal law doesn't overstep the restrictions on federal power outlined elsewhere in the Constitution. The wording is "the Laws of the United States which shall be made in Pursuance [of the Constitution]".
If you follow federal law over state law, but then a federal judge holds that the federal law you followed was an unconstitutional overstep in a domain that the Constitution reserves to the states, you are SOL
This might be happening with the founders of Kalshi. The federal law and CFTC has been saying that these prediction markets are federally regulated, but they're facing criminal charges in some states.
Even that causes problems though as normal casinos with sports betting are then offering a cftc regulated product without a license.
Kalshi isn't "bets", it's a "market" where people trade contracts related to the outcome of the sports game. I think that's the argued legal distinction.
I think it's nonsense and that gambling is very destructive, but there does seem to be a line there where sometimes sports betting is betting, and other times it's trading in a market.
You're assuming the contradiction is between a federal law and a state law and not e.g. a law of the US and a law of France.
One of the more recent fun absurdities is some jurisdictions claiming that if you have a service accessible over the internet then you're subject to their (i.e. every) jurisdiction.
Do you have some examples of an "X" activity or behavior? I understand the logic you're discussing, but can you help ground it?
Suppose you have a law that says that in order to build new multi-unit housing, a given percentage of the new units have to be affordable housing and have to be built within reasonable distance of a transit stop in the same town. Meanwhile you have a town with poor mass transit and very little land zoned for multi-unit housing, and none of it overlaps. In other words, you're both required to and prohibited from building new affordable housing units near a transit stop. Which means you also can't build the other units.
I thought one law could not force you to break another?
Which law are you breaking if you build no housing whatsoever?
Notice that there are many cases of this where that kind of outcome is what you want, e.g. if there is a law against operating e-bikes above 20 MPH and a law against going below 40 MPH on the freeway and the de facto result is "no e-bikes on the freeway" then that's a pretty reasonable outcome.
Whereas "no new housing" is a presumably unintended absurdity, but that doesn't mean you're guaranteed a way out of it.
There are also many cases where rather than being required to do something impossible you're required to do something infeasible, which in practice is the same thing but then they get to point to the entire mountain of shit you'd be required to eat and suggest that you do that.
What are the books in particular? I liked Accelerando and was intrigued by the reputation markets mentioned.
Accelerando was the one I was thinking of. I believe he has some other short stories with Manfred Macx, but I'm not finding them on my shelf immediately.
The Jennifer Morgue comes to mind.
My understanding is that consistency is explicitly not a goal of the American legal system.
Laws are designed to give law enforcement latitude to pursue the charges they seem fit, subject to the taste of a judge.
https://en.wikipedia.org/wiki/I_know_it_when_I_see_it
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.
I just think the team did a good job from what I’m reading. This inconsistency doesn’t impact the top 1% household (who commonly use larger loopholes to avoid taxation at magnitudes more significant than this inconsistency like using loan against assets which they can write off interest against taxes instead of paying taxes to the government). This quirk impacts households in the 2% level for just one fiscal year or more where they might just have a taxed event like a real estate sale (non reinvested primary within the timeline), a taxable equity grant (that the pay taxes on but may lose), one time capital gains from investment sales, etc.
Tax law is supposed to be consistent and fair in general, and the introduction of the Big Beautiful Bill created a weird quirk here, that gets quirkier that you can file separately and correct to jointly but not the other way around legally right now. From 2018–2024, the tax code was consistent on SALT, then in 2025 and looking forward to 2029 SALT taxation becomes inconsistent under certain joint filing conditions that impact a non-trivial number of households especially when it starts at $250k each, or a lopsided earnings of that combined amount and peaks at the $600k.
This team is identifying a pretty big quirk that goes against the principle of consistency in tax law and did a very good job of it applying formal logic to law if they prove this to be correct. Others have done too before AI (which is what your tax software is conservatively doing), but it’s just easier now with AI.
> I just think the team did a good job from what I’m reading. This inconsistency doesn’t impact the top 1% household (who commonly use larger loopholes to avoid taxation at magnitudes more significant than this inconsistency like using loan against assets which they can write off interest against taxes instead of paying taxes to the government). This quirk impacts households in the 2% level for just one fiscal year or more where they might just have a taxed event like a real estate sale (non reinvested primary within the timeline), a taxable equity grant (that the pay taxes on but may lose), one time capital gains from investment sales, etc.
The top 1% have a significant portion of high-income W2 earners who basically have been forced into the standard deduction since the TCJA. It definitely impacts them because that's exactly what the SALT cap was designed to do.
The business owners (lawyers, dentists, investment bankers) are the ones that have all the fun tax breaks, and they're probably more like top-0.1%.
It might be a few people nationwide, but it's a whole lot of families in the Bay Area, New York, Los Angeles, and a few other major cities.
The law was specifically designed to punish these people. Remember, at first they wanted to drop the SALT deduction completely to punish blue states.
Edit: It seems that people are assuming I'm against removing the SALT deduction. Far from it. I am glad they got it done despite being a political third rail for a long time. And despite being a huge beneficiary of the SALT deductions myself.
I don't think people choosing to live in high tax states should get to save on their federal income taxes.
Those people should be taxed a lot.
Why? You're not adjusting for cost of living.
A family making $300k in Manhattan should not be taxed a lot, unless you think a family making ~$115k in Montgomery, Alabama should also be taxed a lot.
Policy is best written by the informed rather than the emotional.
I live in a borderline HCOL/VHCOL city, and arguments like this get thrown around a lot on local boards. But yet the median household income is right around 100k.
People on sites like this tend to have a skewed view of normal.
Also we're discussing a household income of 600k+, not 300k.
Median income != Livable income
Livable income = income that pays for (housing, food, clothing, transportation, medical preventative care and treatment, an emergency fund) x 4
( x 2 for retirement savings without assumption of unbounded economic growth, x 2 for government stealing half your money [1])
I don't think the median is making that number. So that's not the number I'd go off of.
[1] pre-emptive note to shut up the people who will inevitably come to this forum just to lecture me that taxes aren't that high. they are. a LOT of government money-stealing is hidden into things that aren't paid in April, and things that aren't explicitly labelled as taxes.
If you're going to claim that literally half the households living in a city aren't making a livable wage, then I'm going to claim you're exactly the type of person I'm describing who has a cushier view of livable wage than reality.
I agree that your definition is a comfortable living, but that's not reality for the majority of americans.
I assure you that a married couple making 600k a year has plenty of money.
Also, the government stealing half of your money is a ridiculous over-exaggeration. This year my MFJ household income will be around $950,000. My effective tax rate is nowhere near 50%.
This is about a family earning $600,000/yr.
Maybe read correctly before you start complaining. It was 300k EACH, so 600k
No, you should be taxed a lot. [edit: you just said "those people should be taxed a lot" with no reason and then people get sad when the same is said to them]
I agree. I never said they shouldn't.
Don’t tax the rich (and yes, 600k for a couple per year is absolutely rich territory)? “They need to pay their fair share!” Tax the rich? “They’re targeting people in blue cities!”
The SALT deduction is nonsense. Why should high tax states effectively be able to take money from the federal government?
States should be encouraged to provide services to their citizens and reduce burden on federal programs, allowing SALT write offs is part of that. This should be a "win" for all the smaller fed government folks many states are not taxing at appropriate levels and then take a bunch of federal money.
It's funny that me pointing out the fact removing the SALT deduction was meant to punish rich people makes people think I don't like it.
In fact, I was glad they got it done. The Dems didn't object very hard because they knew it had to go too. It's interesting that they didn't put it back when they had the chance.
I don't think the federal government should lose money when people choose to live in high tax states. And I pay high taxes in a high tax state.
It’s even more nuanced than that. The no income tax states like Florida get supplemented more from the federal government. So fed taxes with SALT limits are relatively shifting even more burden to the residence of states who tax their residence and pay for their own local services, which then having to do pay more of the burden for no income tax states.
Making $300k _where_, though?
$300k in NYC is $115k in Alabama.
https://imgur.com/a/1rInLQB
It's 600k. 300k each
So in other words, we're talking about someone making 230k in Alabama?
But isn't that an undue burden on "job creators" with proportionately far-reaching downstream economic consequences?
/s
The tax code has significantly punished dual-income married couples for quite a while. It presumably started some time in the 20th century as some sexists not wanting women in the workplace and then continued because changing it to have them pay the same taxes as they would if they were unmarried would result in a significant reduction in government revenue.
This isn't really a punishment. You can choose to file separately. You just pick the option that leads to the least tax.
Thank you for posting this!
There's whole language for law formalization called Catala.
See https://catala-lang.org/
and https://github.com/CatalaLang/catala-examples
French government seems to actually use it in one of their web services, see https://docs.aides.beta.gouv.fr/03_mutualiser/02_outils.html (page in French)
> Today, we set out to formalize the entire Internal Revenue Code to hunt for unknown loopholes (bugs).
Saying that loopholes are bugs is a political statement that a particular allocation of resources is inherently fraudulent. There is no data that Lean code could use to decide whether a result is intentional or not.
It's like deciding that any tax provision that increases income inequality is illegitimate, and writing code to identify them. That could be a useful exercise, but it isn't a way to justify a human value with math. It may be a formalization of an ethic as applied to a tax code, but not of the tax code.
Any change to the law that bill authors have to hide by phrasing the bill so that it sounds like the change is otherwise is illegitimate, and that's what formalization is meant to catch.
I suppose, but most of the times loopholes aren't like that.
Either they are intentional things that have unintended consequences or they are unintentional things that people didn't realize what they meant.
Sometimes they are just laws that are working as intended but somebody doesn't like them so they are labelled as a loophole.
I think there are very few loopholes that people intended to create by intentionally phrasing it weirdly.
I think there are more such loopholes than most people realize.
From The Blind Spot: How Oligarchs Dominate Our Democracy by Jeffrey Winters: "When it comes to winning advantages for wealthy and powerful clients, lobbyists focus in on micro-details no one else is paying attention to but which could mean millions or billions saved by clients. 'Sometimes we were changing a word and that's all that we needed,' one lobbyist admitted."
But some of the "bugs" do seem to be weird complex misalignments rather than directed tactics.
Agreed. In fact, you'll see things termed loopholes vs. benefits depending entirely on politics so it can't be a property of the law itself. An EV tax credit or SALT deduction are "loopholes" too.
It's important to remember that the loopholes are often intentional. They are left there so that rich people who can afford CPAs can take advantage of them, while middle income and poor people cannot afford to.
They are also left there so there is wiggle room for interpretation if it comes in front of an auditor or a judge.
And also, it's important to remember that in tax matters, the final arbiter of interpretation is a judge. Judges are humans, not machines. You can't "Trick" them by saying "well technically this is allowed!". Because they rule on the sprit of the law, not as it was written. Judges aren't amused when you try to be cute with how you interpret a law. And some Judges have biases, where you get a different ruling depending on if you play at their golf club or not.
Laws aren't computer code. They are vague on purpose.
I've heard this repeated a couple times here on HN. Do you have any citations for laws being vague on purpose? The whole point of laws, and the formal structure they take, is to reduce vagueness. Is this rock on person A's land or person B's land? When it turns out, despite best efforts, that a law is vague we even have a second system to step in and reduce the vagueness further: case law. I have no doubt that people are trying to exploit vagueness on both sides, but naysaying here is nonsense. And almost nobody wants law to be vague either.
Lawyer here (but I don't make any money from it and absolutely have no dog in this fight). I agree. Law is vague for two reasons - first it is often as a compromise between two positions that people were okay having decided on a case by case basis instead of fighting to the death over what to write down. It also is vague sometimes to intentionally capture the spirit of what it is trying to do. While I won't claim vagueness is never left to benefit someone ( I'm sure it happens), I would claim it is rare.
Law is basically a representation of societal judgement. While criminal law is intended to be clear enough to know when you've violated it, that is not the same as beimg logical or consistent. Civil law is even less logical and consistent. Formalizing it into logic generally does not make sense overall - it isn't really broken in most cases because it was never intended to be totally consistent. There are certainly areas that could use cleaner rewriting but courts are generally well equipped to figure out what it means. Congress and the states can always overturn interpretations of law, but the rate at which they rewrite laws because they thought courts interpreted it wrong is very, very low.
He’s half correct.
They are intentional.
They aren’t loopholes. They are just laws.
Some people just call them loopholes because they dont like them.
Much of the US Constitution is vague or "general."
There are quotes from at least Madison, Hamilton, and Jefferson that support the idea that this was intentional.
I do agree with the main point though: laws shouldn't be vague and also case law tends to refine the meaning.
All overly broad generalizations are vague on purpose
> And also, it's important to remember that in tax matters, the final arbiter of interpretation is a judge. Judges are humans, not machines. You can't "Trick" them by saying "well technically this is allowed!". Because they rule on the sprit of the law, not as it was written. Judges aren't amused when you try to be cute with how you interpret a law. And some Judges have biases, where you get a different ruling depending on if you play at their golf club or not.
> Laws aren't computer code. They are vague on purpose.
Yes... but. Tax law is a bit different because it is similar to an equation: you put in your inputs and you get your outputs.
There have been famous cases where the courts have said in essence, "yes you completely and exactly and precisely followed the law, but we're not going to allow you to do that anyway." Those rulings have become less frequent.
The fact that you need a judge to tell you if what you did was wrong is indicative of a flawed system
No it is not a flawed system. That is literally the legal system at work (at least the Westminster / US systems with judge-developed case law). Legislature writes the law, and nobody knows for sure what constitutes "complying with or being in breach of that law" until judiciary rules on it (sometimes decades later!).
This is ridiculous - first of all you don’t have to be rich to afford a CPA, second of all high earners almost always pay the highest rates (both effective and marginal). And even in the cases where they don’t pay huge marginal rates (dividends and LTCG), they don’t need a CPA to take advantage of that because it’s dead simple.
https://taxfoundation.org/data/all/federal/latest-federal-in...
I'm not talking about a high earner who makes a few hundred thousand a year. I'm talking about the high earner who is making a few million a year and taking advantage of the vague tax laws by paying a CPA tens of thousands of dollars to do their returns for them and then save them a few hundred thousand in taxes.
And yes I'm aware that the wealthy pay most of the taxes. I'm fine with that. I'm just pointing out that these laws are made so they still pay less than they would otherwise.
It depends on how you are making these millions. A W-2 employee at meta making $1M or more per year is almost certainly paying over 50% marginal tax rates (combined state and federal). And there is virtually nothing you can do to lower that burden by any significant amount.
The tax code benefits certain types of income, but it does not uniformly benefit high earners, as you say.
How does that scheme work? Which provisions are you talking about?
I don’t know I’m not a CPA. That’s why I hire one. Because the tax code is too complex and vague to do it myself.
> Because they rule on the sprit of the law, not as it was written.
I feel like this attitude is responsible for the modern destruction of the rule of law.
It doesn't matter what the law says, the only thing that matters is vibes! And whether you play golf with the right government officials.
> You can't "Trick" them by saying "well technically this is allowed!".
The obvious problem being that sometimes it is allowed. And then do you want that being decided by democratically elected representatives and specified ahead of time so the public can know what's expected of them and of others, or decided ex post facto on the basis of feels and discrimination?
> Because they rule on the sprit of the law, not as it was written.
Extremely funny to say that about US law when it is entirely based on precedent, and a single judge having vibes on a particular day changes how your entire country works for the next 50 years.
US law is explicitly made to be skirted, as is every common law system in the world and they are all irrevocably flawed.
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?
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.
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.
This is the case where the xkcd doesn't apply though.
The thing about insurance fraud is that the major thing that will cause it to be fraud is when you set the fire on purpose.
The tax code doesn't really have that. You'll often even see confused people inserting nonsense language in various places to the effect that doing something to avoid taxes isn't allowed, but meanwhile "doing something to avoid taxes" is the expected mechanism of operation for tax incentives meant to get people to do something they otherwise wouldn't have done.
And then because of that you need to actually care about what the tax code says and what the unnecessarily complicated nonsense allows someone to get away with without breaking the law, instead of pretending that it's all common sense and people can be punished for being "bad" without ever actually specifying what that means.
You wouldn’t be proving the tax code, you’re proving that a procedure follows the tax code. This way you’d be able to know for certain if an AI that tried reducing your taxes actually gives you a valid procedure/result, assuming you can trust the Lean formalization (hint: you can’t given the nature of law, especially if it’s vibe coded like this)
Maybe you could validate stuff, like "how much would I be taxed if I did X" and then have it come up with all the questions that need to be answered to determine the answer or "what's the max I could be taxed if I did Y"?
I don't know much about Lean, but I assume that beyond proving things it functions as a truth graph you could walk to calculate things...
Edit, it might also be (someday) useful when drafting tax law to make sure the law is actually sound (e.g. isn't contradicting something else) or to see what it's overlapping with?
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 guess by powerful they mean with a lot of power over its citizens.
we need detector vans, for logic!
I'm struck by this:
"The comparison caught ... mistakes in our own model too. We had not counted self-employment profit toward the 20% deduction for small-business income"
This seems like a pretty big oversight? Makes it feel like there might be a lot more low-hanging fruit, much less subtitles to explore?
This is only like the fifteenth vibecoded “formalization” of some set of laws I’ve seen on HN that get posted just to be abandoned in a few months.
If the tax law is inconsistent (as some of the comments seem to indicate), does that mean that we don't have to pay any tax or even are entitled to a large tax credit? After all, Lean supports the principle of explosion (https://en.wikipedia.org/wiki/Principle_of_explosion).
interesting idea. the concept of formalizing legal code is attractive to me, if only because i am addicted to logic. but realistically this will be hard to extend past tax code. formalization of law is more difficult in common law, which is heavily driven by judicial presedent, which is fluid and resists codification. a machine learning algo trained on cases might perform better, but even then, so many cases cant be determined easily.
I've been reading a very sobering book that came out this year, The Blind Spot: How Oligarchs Dominate Our Democracy and what I've read tells me that for the people who are running things the loopholes are features and not bugs. I strongly recommend this book. Things like Nixon's sabotage of the IRS, the revolving door of employment in US Treasury and private tax law firms, the labyrinthine nesting of partnerships inside pass-through partnerships—it's shocking stuff.
this is actually wonderful. and a good use of the tech. ive been joking about wanting to do this for years, but the sheer magnitude of work made it impossible for me to consider doing
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.