As a proof-of-concept, I've been using extra tokens to formalize the IRS tax forms and worksheets, mostly just to prove this can be done. The idea is that something like this could be adapted into a publicly maintained version of the IRS Direct File program (RIP). I'm up to an estimated 60% coverage of US federal tax situations so far.
That's very cool but don't you think the Big AI labs will soon have collected enough data from us that they can easily do this?
That's neat, what aspect(s) are you formalizing? That a given tax statement is correct?