RGS1811

This is gorgeous! Great idea!

That's the dream!

It's also something that can be made more achievable by pruning coverage to the most common tax situations. E.g. my target coverage for this project is 80% of federal filers, individuals only. This is a lot more achievable than achieving coverage for all individuals plus businesses, etc.

Thanks so much!

You just mail them in!

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

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.

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.

> Just use the LLM to make a thing that's actually good at what you need it to do.

This is the end state of most imagined use cases for “agentic” software IMO. Use the AI to build software, with a classifier or LLM as the expansion joint in awkward spots.

5

I love it. The graphing tool is awesome.