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?

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?

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)

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

[flagged]