Hacker News

points by RGS1811 1 day ago | 0 comments

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

[–] dang 11 hours ago

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

[–] RGS1811 11 hours ago

Thanks so much!

[–] darksim905 1 day ago

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.

[–] timcobb 1 day ago

That's neat, what aspect(s) are you formalizing? That a given tax statement is correct?

[–] RGS1811 1 day ago

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.

[–] celestialcheese 1 day ago

The IRS open sourced their direct-file code after it got cut. IIRC similar work done there. https://github.com/IRS-Public/direct-file

[–] dang 11 hours ago

One past thread:

IRS Direct File - https://news.ycombinator.com/item?id=44131901 - May 2025 (65 comments)

[–] timcobb 15 hours ago

IRS fillable forms is really good in my opinion it should be more widely known.

[–] Onavo 1 day ago

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.

[–] vatsachak 1 day ago

Nice. Is the lean used to formalize formulas?

[–] RGS1811 1 day ago

Sort of. The formulas for each line live in the form YAML I described above. The formulas are built out of a set of primitive operations that are defined in lean, with their properties proved there (non-negativity, monotonicity, etc.). There's also a lean evaluator that's run on compiled form data and cross checked with the typescript evaluator. (There's a lot more detail in the README.)

[–] vatsachak 1 day ago

Nice. Opus 5.5 is crazy good at engineering ideas into life. Really cool stuff, using "code is data" with Lean

[–] gbacon 1 day ago

You are one sick puppy. This is a brilliant idea.

[–] c0nsumer 1 day ago

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.

[–] amelius 1 day ago

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?

[–] RGS1811 1 day ago

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.

[–] singhrac 1 day ago

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!

[–] tosser811 1 day ago

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.

[–] ToucanLoucan 1 day ago

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?

[–] RGS1811 1 day ago

You just mail them in!

[–] ordersofmag 1 day ago

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

[–] ToucanLoucan 17 hours ago

Ohhhh I thought Direct File included the mail-in options, not just the online one. Thank you!

[–] ryandrake 1 day ago

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.

[–] rbhelt 1 day ago

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

[–] ClikeX 1 day ago

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.

[–] rbhelt 1 day ago

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.

[–] what 1 day ago

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.

[–] thenewnewguy 1 day ago

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?

[–] singron 1 day ago

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

[–] NichoPaolucci 1 day ago

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)

[–] amelius 1 day ago

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

[–] tclancy 1 day ago

[citation needed]

[–] fn-mote 1 day ago

Plus there is little chance it will be done in the future by any large entity because of the entrenched interested in the area.

[–] Xcelerate 1 day ago

This is amazing. I’ve wanted something like this for a long time. I’d pay for it even.

[–] ForHackernews 1 day ago

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.

[–] RGS1811 16 hours ago

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/