The legal system, famously completely deterministic with no human-judgement element whatsoever and therefore modelable as computer code.

LLMs, famously super reliable in the legal field.

sits down with a biiig bucket of popcorn

I can't wait for somebody to actually try to argue a case with this.

Also, a lot of things people refer to as tax loopholes aren't actually gaps in logic. A lot of them are things that exist for a logical reason, but are being applied in a way that isn't intentional.

Things like "I own a convenience store, my wife and kids work there" which then gets used when some billionaire spins up a subcontractor of his business, hires his wife and kids as the only employees, and then assigns his house as an asset owned by that business and uses it to siphon away expenses or whatever.

I'm not a tax lawyer either 😛, but the point is that a lot of the loopholes exist for a sensible purpose, but are being chained or applied outside their original purpose.

Formalizing =/= proof. There's nothing to prove. Don't change the headline if you don't know what you're talking about.

Also it's funny how this formalization reveals MANY inconsistencies in the law. I have no doubt that the legal system is formally a huge turd. Imagine if they did this for the death penalty. Too bad these computers are controlled by the ultra privileged. Ofc they're trying to dodge taxes.

Skimming this, it's not clear to me what exactly is being done in Lean. It sounds like an LLM is translating the tax code into lean and then using those lean statements. But the translation step is highly error prone. Tax codes are not mathematically complicated (which is what Lean is good for) but logically complicated (which LLMs suck at)

Maybe someone with more patience can chime in

formal methods will always have a huge place in my heart