Hacker News new | past | comments | ask | show | jobs | submit
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.

https://github.com/emmilco/us-tax-model

That's interesting! I've re-upped your Show HN (https://news.ycombinator.com/item?id=50278678) using HN's second-chance mechanism (described https://news.ycombinator.com/item?id=26998308).

(Posting here since we don't have another way to contact you, and of course that thread will be better with you in it...)

loading story #50294870
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.
That's neat, what aspect(s) are you formalizing? That a given tax statement is correct?
Not quite. The formalization covers the IRS's published procedure, i.e. the questions and calculations that go into the published forms, worksheets, and instructions. It's not a formalization of the tax code itself, and it's not a tax calculator, though a client of the underlying code could function as a tax calculator. (The project includes such a client, a CLI tax interviewer, just to exercise the code.)

In more detail:

- every line of every form gets a YAML representation which includes the source text, a data type, and an expression built from a small set of lean atoms, plus a citation pointing to the exact location of the rule in the original official document.

- underneath the yaml layer there's a lean formalization of the atoms showing that they behave as specified, that all comuptations use only the allowed atoms and operations, etc. There's also a typescript evaluator that's used to cross check the lean for agreement, so we have the arithmetic represented two ways.

The critical failure point for an LLM-produced formalization like this is the interpretation of the form text. Since I'm not a tax lawyer and don't intend to become one, this is an explicitly owned weakness and one I've structured the project around. Publicly available tax calculators (PolicyEngine, UsTaxes, OpenTaxSolver, etc.) are used to cross check derived numbers from this system. Mutation testing ensures the test suite is robust against bugs and arithmetic errors. Interpretations are cross checked by different model families (Claude, GPT, Deepseek). Etc.

The idea is to derive confidence from the formal properties of the system itself, and to allow theoretical future users of such a system to derive confidence in the interpretation of specific forms by making it easy to cross check line-level formalizations against the source documents.

There's a lot more detail in the (alas, Claude-authored) README. When I have time I'm going to write my own version of the README expressing my vision of the project, but I'm not there yet.

loading story #50285285
loading story #50290519
Some of the interpretations won't be correct without grounding them in old case law. That's the expensive part, in many jurisdictions, the official interpretations by the tax department are not free.
loading story #50279651
I recently did something similar, using Claude Code to formalize a set of rules for a sporting event as part of building a computer-based scoring system. It's worked very well.
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?
I'm not sure it matters. The IRS killed Direct File under lobbying pressure from the tax prep industry. In my opinion the public is owed a free version of this sort of tool. If the IRS doesn't produce it, then citizens ought to. If Google or Anthropic or whoever wants to offer a free version of this, more power to them, but I don't see why they'd bother. They could have done it decades ago.

And to be clear: my vision here isn't "have an agent do your taxes", it's to have agents build a hardened and thoroughly verified deterministic tool that can help you navigate the (somewhat bewildering) forms and instructions decision tree when filing your own taxes.

This is great, and I appreciate the approach. Yes, tax calculation should be a decision tree. Unfortunately it is truly pretty complicated (just this year I had to abandon FreeTaxUSA for TurboTax because the latter handled an important case I needed better). But I have a lot of faith that we can do this right. Good luck!
Funny, after 10+ years of using TurboTax Online I moved to FreeTaxUSA last year and it's like a breath of fresh air. TurboTax couldn't do what I needed to do (e-file a late return) and FreeTaxUSA had no problem with doing that.
I have a probably stupid question: given that the IRS killed Direct File, even if your software can create ready-to-file (or even ones that need some work) tax returns, isn't that moot without a way to like... get the IRS to accept them?
You just mail them in!
If your software can fill out the forms then you can (at the very least) print them and mail them in. The IRS certainly still accepts that.

https://www.irs.gov/filing/where-to-file-paper-tax-returns-w...

Ohhhh I thought Direct File included the mail-in options, not just the online one. Thank you!
Why wouldn't the IRS accept a tax return created by your own software? How would they even know it was custom software? Ultimately your tax return is just a stack of papers that gets sent to the IRS.
Software sending efiles to the IRS has to be tested with and approved by the IRS. The IRS is working toward eliminating paper filing as an option. At this point, paid preparers are legally required to efile all returns and if the return gets rejected and they must paper file, they have to include Form 8948, Explanation for Paper Filing. For the IRS to accept a tax return from software the software has to go through this process. https://www.irs.gov/e-file-providers/how-tax-preparation-sof...
As someone from the Netherlands, this is bonkers to me. I just log in to the tax site, review what they've already filled in for me, and submit.
It is truly insane. Major corporations spent billions to prevent this. The worst part is that for the majority of Americans, the government has already internally prepared their tax return before they even file but again the tax preparation industry spends a fortune lobbying Congress to prevent an automatic filing of taxes.
I think you meant to say they spent billions to create this?

In either case the tax prep industry is a pox on our society. But of course this is America, and replacing a perfectly functioning publicly accessible service with a nightmare of private sector bullshit is the most violently American shit ever.

As an American, it is bonkers to me too. Last year my former employer did not issue me a w-2. I called the IRS to ask them what to do. They said they had all the information but can’t release it to me until after the filing deadline. Instead I was told to use form 4852 to estimate and file an amended return if my estimate was wrong once they give me the numbers they have. Worst part is you can’t efile when you file with form 4852.

Anyway, my point is that for 95% of people they have all the information already and you shouldn’t have to file.

This! I am CPA with a tax practice and it makes me unreasonably angry that the tax prep industrial complex has lobbied our government into making the vast majority of people stress over their tax returns or have to pay someone to prepare a return that is already sitting on an IRS computer. No CPA worth their salt wants to do the simple returns but companies like Intuit and HR Block feed off them.
The first option on Form 8948 is "Taxpayer chose to file this return on paper" - is there any evidence paper filing is going away permanently?
You can use free file fillable forms to submit online. It's a bit of work to transcribe from other software. It also requires a particular interpretation when filling forms (e.g. you need to round before summing your W-2s).
I think that assuming work can be done more easily in the future should not stop people from doing work that needs to be done in the present.

(If a painter knew that the camera was coming out I would not want them to throw their canvas away)

> (If a painter knew that the camera was coming out I would not want them to throw their canvas away)

That's not a fair comparison because the painter produces different work, whereas tax computations will be the same.

[citation needed]
Plus there is little chance it will be done in the future by any large entity because of the entrenched interested in the area.
This is amazing. I’ve wanted something like this for a long time. I’d pay for it even.
I think the IRS already did some version of this and open sourced it https://github.com/IRS-Public/fact-graph

There's an article about it here https://biggo.com/news/202510160717_IRS-Fact-Graph-Public-Re...

These were artifacts from the IRS Direct File program (RIP)

Maybe your project could (re)productionize this dataset.

When I was planning the project, I looked into FactGraph to see if it'd be worth building on. I opted not to for a few reasons:

- It's oriented toward the IRS's internal XML API in a way that's not really useful for this project, since no consumer of my code is going to digitally submit to the IRS.

- The semantics of FactGraph are largely undefined, and the maintainers themselves seem to acknowledge that its development trajectory went off in a bad direction and it needs major divisions.

- It's super verbose.

- It's the year of Lean, so I wanted to find an excuse to use Lean.

Other work has been done in this domain, though. The biggest example is Catala[0], though Prof. Sarah Lawsky at Northwestern seems to have made some strides toward formalizing the Internal Revenue Code.

[0] https://catala-lang.org/