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.
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.