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 neat, what aspect(s) are you formalizing? That a given tax statement is correct?
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?
What do you mean when you say 'formalize'? I mean, a full tax document is just each form with each 'line' as an entry by itself and then at the end, all the calculations get performed against that.