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?

▲

squirrel 3 hours ago | parent | next [-]

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.

▲

claw-el 3 hours ago | parent | prev | next [-]

Maybe tax change impact analysis by congress can easily be calculated using Lean. The article also said loopholes can be easily identified?

▲

marcta 3 hours ago | parent [-]

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.

	▲	AnthonyMouse 2 hours ago \| parent [-]
		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.

▲

chrisnight 2 hours ago | parent | prev | next [-]

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)

▲

rendaw an hour ago | parent | prev | next [-]

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?

▲

realistically_c 3 hours ago | parent | prev | next [-]

this is actually a really bad idea and is the opposite of what a powerful state would want

▲

2 hours ago | parent | next [-]

[deleted]

▲

convolvatron 3 hours ago | parent | prev [-]

maybe some rationale? states should want to preclude people from reasoning about tax laws?

▲

Xirdus 3 hours ago | parent [-]

I guess by powerful they mean with a lot of power over its citizens.

	▲	convolvatron 3 hours ago \| parent [-]
		we need detector vans, for logic!

▲

luxiedge 3 hours ago | parent | prev [-]

[flagged]