Formalizing US Tax Code (Using Lean)

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.

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.

> 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 provision 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.

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)

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'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?

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?

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.

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.