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?