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.