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)
Lean helps a lot in formalising advanced mathematics, because it is able to express statements and proofs of that mathematics in a way that most tools can’t, and it can be checked by computer. It doesn’t help much in formalising logically complicated scenarios because you can express those in any old formal language.
If your tax bill depended on the convergence of some gnarly integral, Lean would be great. But it doesn’t; it depends on a billion bits of trivial mathematics composed together with rules that combine to be ambiguous and complicated. No computer environment helps with the ambiguity, whilst any computer environment can formalise that complication once an interpretation has been chosen.
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
Lean is more than capable of modeling logic.
Lean is capable of modeling formal logic. The jump to legal “logic” is highly questionable.
Not really my point, but sure.
Then what was your point?
Lean helps a lot in formalising advanced mathematics, because it is able to express statements and proofs of that mathematics in a way that most tools can’t, and it can be checked by computer. It doesn’t help much in formalising logically complicated scenarios because you can express those in any old formal language.
If your tax bill depended on the convergence of some gnarly integral, Lean would be great. But it doesn’t; it depends on a billion bits of trivial mathematics composed together with rules that combine to be ambiguous and complicated. No computer environment helps with the ambiguity, whilst any computer environment can formalise that complication once an interpretation has been chosen.
So what formal language do you think would be more appropriate than Lean for this purpose?
PHP.
Half kidding, but you’re asking the wrong questions. Go read my original comment again.