RGS1811

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.

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

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

I converted my post-it based task tracker to an iOS app. It has no subscription, no data leaves your phone, and it costs 2 USD. It’s got no AI features but you can add tasks with siri by way of a shortcut.

Much less ambitious than what 3anddone is trying to do. But If you’re interested, check it out. It’s called “Grask”.

Forgive the ignorance, but how are you running a 763B parameter model on 64GB of RAM?

How is the ability of a human to understand the code via hands-on familiarity not a direct dependency of their ability to do manual code review? I don't get it. Having claude write an explainer (something I do a lot!) doesn't get you to the point where you can confidently assess a complex diff. And you've funneled your priors on what the diff says and does through the same system that already reviewed and approved it. This article isn't bad but it doesn't give enough weight to the human context-building part of the problem.

I guess I'd say that your qualia aren't a something, but they're not a nothing either. We can't say what they are. They're not publicly describable, and therefore not publicly attributable. As Wittgenstein would say, "They cancel out."

And as I think Dennett himself would say, qualia are just Sellars's Given rearing its ugly head again.

I actually agree with you. LLMs could become participants in the future, but this would require (1) durability of real awareness over time (an architecture change from the current fixed-weights + transient context architecture) and (2) that humans grant them the status of equal participants (probably not a terribly high bar given how people already treat these things). I'm not aware of any real progress toward (1), and all the stand-ins people have developed live in the context layer or textual artifacts, which are poor stand-ins for durable memory.

And yeah, consciousness based arguments are bunk IMO. It's clear that LLMs are in a basic sense "aware", and even to some extent "sapient" (in Brandom's usage), i.e. they can justify claims and object to things at least locally. I follow Rorty on the question of consciousness, which is to say that consciousness has no deeper meaning in practice beyond "are you awake", and in philosophical discussion it's largely a proxy for "are you one of us" in some amorphous sense.

Brandom wrote a shorter version of the book, called "Articulating Reasons", which is available in full on his faculty page [1], or from booksellers. He's a very wordy writer (kind of exhausting to read, even for someone who enjoys philosophy), but if you get ahold of Making It Explicit, chapters 2 and 3 have the meat of the ideas I'm talking about here.

[1] https://sites.pitt.edu/~rbrandom/Courses/2022%20Phil%20of%20...

Edit: One of my ways of benchmarking new AI models is actually to type a version of this prompt in and see how sophisticated the response is: "Talk to me about the concept of deontic scorekeeping in the context of llms". You'll get good mileage out of that.

Recursive self improvement is a bulk process that shapes the weights of the next model. The weights are still frozen. Each individual "agent" would need to able to durably update its own dispositions to get to what I'm talking about.

I'm not suggesting mathematics and language are the same thing, but I am saying (which shouldn't be controversial) that mathematics as a discipline exists within the medium of language, and that mathematical reasoning, discovery, and proof happen via people proposing, justifying, testing, and objecting to formulations in language. This isn't a metaphysical claim about whether math is real or captures inherent structures of the universe etc.

The irony of complaining about an academic jargon word in a thread about mathematicians.

Because language is mimetic, and people are consuming huge quantities of AI-generated text. I.e. saying that an LLM can't be an equal participant in our language games isn't saying that it can't play by the rules. In fact that's what LLMs are trained to be best at.

What an LLM can't do (at least with the current architecture) is sustain a commitment that it can be held accountable for later. It doesn't have durable "perspective". It can't update its priors. Maybe a new architecture will come along that gives LLMs memory plasticity, at which point they will shift into being individuated quasi-persons, but that's not what we've got now.

I've written some about this here, if you're interested: https://elliotmilco.substack.com/p/deontic-scorekeeping-comm...

This piece circles, without naming it, around the concept of “deontic scorekeeping” central to the work of Robert Brandom on semantics. The idea that our ability to create and sustain conceptual systems depends on the give and take of reasons within a social setting. Brandom has been front of mind for me lately because elements of his theory both explain why LLMs should work in principle, and where they are bound to be radically deficient. An LLM encodes the normative regularities of our linguistic/conceptual games into its weights, but it cannot be a real participant in our games because it is incapable of staking durable commitments or changing its dispositions over time.

Worth reading: Robert Brandom, “Making It Explicit: Reasoning, Representing, and Discursive Commitment”

- I clicked "try in gemini", typed a prompt, got an unimpressive result.

- Then I realized Gemini 3 was active.

- I tried switching models.

- I was presented with a $99/mo subscription offering.

- I scrolled down and clicked to get cheaper options.

- I chose the $19.99 "AI Pro" monthly option and paid.

- In chat I was able to use Argon. Cool. Seems pretty smart.

- I asked Argon if I could use it through opencode with my Google account.

- Argon said yes, but then told me I'd have to use the Gemini CLI as middleman.

- I told it I didn't know there was a CLI for Gemini; I'd just use that.

- It told me how to install gemini-cli.

- I authenticate via Google OAuth inside gemini-cli.

- Gemini-cli rejects my login, says the app is deprecated for subscription users, who must use agy.

- I install agy.

- In agy, I open the model selection menu.

- "Gemini 4 Argon is currently available to Ultra plan subscribers." Odd... Gemini 4 Argon is the model (included in my Pro plan) that told me to do this.

- I discover that Claude Opus 5.5 is included in the subscription. I switch to it and give it a debugging task.

- Within about 5 minutes: "Individual quota reached. Please upgrade your subscription to increase your limits."

- This is dumb. Google stole twenty bucks from me; I want my money back.

- I go to the Gemini web app to cancel my subscription. I paid on my phone, so I have to cancel on my phone.

- The Gemini iOS app has a "manage my subscription" page. I go there to manage my subscription.

- This "manage my subscription" page includes no way of cancelling.

- After a minute of confusion I go to the App Store > Subscriptions > Gemini > Cancel.

- My subscription will end at the end of the month (no refund).

- Then I have to find the complaint form so I can request a refund.

- But I did request one.

Anyway, "frontier intelligence" just wasted about an hour of my life.

Name the alternative tech news / user sentiment sources. I want to widen my reading.

I don't see "new" in either of the criteria you quoted. It also doesn't fit with the explicit reasons given for awarding the prize to many past recipients. Sometimes originality is a factor, but in many cases the reason is just judged merit.

Look at the list here: https://en.wikipedia.org/wiki/List_of_Nobel_laureates_in_Lit...

This model finally got me off my Claude Max subscription. I’ve found it superior to Opus 5.5 in certain use cases, and certainly faster.

I’m convinced that I’ll have good enough inference on my laptop at reasonable speeds within the next year.

Why assume that novelty is a criterion for the worth of someone's literary output? Things can tread familiar ground, use familiar forms, and still be remarkable or worthwhile. (Imagine saying to Shakespeare: "Why write a book of love sonnets? Didn't Petrarch already do that?")

That said, I haven't read more than a few pieces by Carson and I'm curious to read more.

I don't really think poetry can reasonably be said to be a genre that's "over promoted by the big labels".

If this is actually based on decompilation, they're going to get sued into oblivion. If it's a reverse engineering project based on behavioral observation... it's probably relatively thin, and the question becomes whether the maintainer(s) are going to invest enough effort into it to merit user trust. Given how massive the feature sprawl of Adobe CC is, getting from zero to something is pretty easy. Maintenance, completeness, and meriting trust are a lot harder.

I find the author’s attitude and approach here really admirable. Lot’s of good ideas in this post.

That beak is CHONKY.

At this point, the scare quotes are well-earned.

It analyzes your text messages and tells you to say "lolol" back to people a lot. Also it periodically swamps the GPU in order to analyze all your photos.

I’m going to be the lone dissenting voice here and say I still find it overeager and irritating to work with.