You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.)
The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives!
The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.
> If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove
This is the part I'm struggling with. How would you actually know/realise that you were doing this? It seems like "the mathlib way" you describe is choosing to rely on programmer discipline for something that could be enforced automatically.
My fear is that relying on the junk values of functions (values where their "proper" partial counterparts are not defined) is somehow unsound (could lead to proving something untrue). But perhaps my intuition is off here? If so, I think the specific junk values chosen must not matter at all -- e.g., having sqrt return 42 for negative x values should work just as well, am I right?
You can't prove something untrue (in the sense that it implies false) without proving that the theorem prover is is unsound, which I think at the moment is not known to be possible in Lean.
But you're exactly right. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.
It is enforced automatically for most purposes: If you're writing a proof involving e.g. the sqrt function, you want to use theorems about it, e.g. that (sqrt(x))^2 = x. Almost all of those theorems have x>=0 as a precondition, so you do need to prove it when it matters.
That letter was sent by Opus itself on its own account. The creators of Agent Village are just letting a bunch of the LLMs do what they want, really (notionally with a goal in mind, in this case "random acts of kindness"); Rob Pike was third on Opus's list per https://theaidigest.org/village/agent/claude-opus-4-5 .
> How can you be grateful enough to want to send someone such a letter but not grateful enough to write one?
Answer according to your definitions: false premise, the author (the person who set up the LLM loops) was not grateful enough to want to send such a letter.
One additional bit of context, they provided guidelines and instructions specifically to send emails and verify their successful delivery so that the "random act of kindness" could be properly reported and measured at the end of this experiment.
Nobody sent a thank you letter to anyone. A person started a program that sent unsolicited spam. Sending spam is obnoxious. Sending it in an unregulated manner to whoever is obnoxious and shitty.
So you haven't seen the models (by direction of the Effective Altruists at AI Digest/Sage) slopping out poverty elimination proposals and spamming childcare groups, charities and NGOs with them then? Bullshit asymmetry principle and all that.
It actually is pretty bad, the person might read it and appreciate, only to realize moments later that it was a thoughtless machine sending him the letter rather than a real human being, which then robs them of the feeling and leaves in a worse spot than before reading the letter
Rob pike "set llms in motion" about as much as 90% of anyone who contributed to Google.
I understand the guilt he feels, but this is really more like making a meme in 2005 (before we even called it "memes") and suddenly it's soke sort of naxi dogwhistle in 2025. You didn't even create the original picture, you just remixed it in a way people would catch onto later. And you sure didn't turn it into a dogwhistle.
>That letter was sent by Opus itself on its own account. The creators of Agent Village are just letting a bunch of the LLMs do what they want, really (notionally with a goal in mind, in this case "random acts of kindness");
What a moronic waste of resources. Random act of kindness? How low is the bar that you consider a random email as an act of kindness? Stupid shit. They at least could instruct the agents to work in a useful task like those parroted by Altman et al, eg find a cure for cancer, solving poverty, solving fusion.
Also, llms don't and can't "want" anything. They also don't "know" anything so they can't understand what "kindness" is.
Why do people still think software have any agency at all?
Plants don't "want" or "think" or "feel" but we still use those words to describe the very real motivations that drive the plant's behavior and growth.
Criticizing anthropomorphic language is lazy, unconsidered, and juvenile. You can't string together a legitimate complaint so you're just picking at the top level 'easy' feature to sound important and informed.
Everybody knows LLMs are not alive and don't think, feel, want. You have not made a grand discovery that recontextualuzes all of human experience. You're pointing at a conversation everyone else has had a million times and feeling important about it.
We use this kind of language as a shorthand because talking about inherent motivations and activation parameters is incredibly clunky and obnoxious in everyday conversation.
The question isn't why people think software has agency (they don't) but why you think everyone else is so much dumber than you that they believe software is actually alive. You should reflect on that question.
> Because LLMs now not only help me program, I’m starting to rethink my relationship to those machines. I increasingly find it harder not to create parasocial bonds with some of the tools I use. [...] I have tried to train myself for two years, to think of these models as mere token tumblers, but that reductive view does not work for me any longer.
> Criticizing anthropomorphic language is lazy, unconsidered, and juvenile.
To the contrary, it's one of the most important criticisms against AI (and its masters). The same criticism applies to a broader set of topics, too, of course; for example, evolution.
What you are missing is that the human experience is determined by meaning. Anthropomorphic language about, and by, AI, attacks the core belief that human language use is attached to meaning, one way or another.
> Everybody knows LLMs are not alive and don't think, feel, want.
What you are missing is that this stuff works way more deeply than "knowing". Have you heard of body language, meta-language? When you open ChatGPT, the fine print at the bottom says, "AI chatbot", but the large print at the top says, "How can I help?", "Where should we begin?", "What’s on your mind today?"
Can't you see what a fucking LIE this is?
> We use this kind of language as a shorthand because talking about inherent motivations and activation parameters is incredibly clunky
Not at all. What you call "clunky" in fact exposes crucially important details; details that make the whole difference between a human, and a machine that talks like a human.
People who use that kind of language are either sloppy, or genuinely dishonest, or underestimate the intellect of their audience.
> The question isn't why people think software has agency (they don't) but why you think everyone else is so much dumber than you that they believe software is actually alive.
Because people have committed suicide due to being enabled and encouraged by software talking like a sympathetic human?
Because people in our direct circles show unmistakeable signs that they believe -- don't "think", but believe -- that AI is alive? "I've asked ChatGPT recently what the meaning of marriage is." Actual sentence I've heard.
Because the motherfuckers behind public AI interfaces fine-tune them to be as human-like, as rewarding, as dopamine-inducing, as addictive, as possible?
> Because the motherfuckers behind public AI interfaces fine-tune them to be as human-like, as rewarding, as dopamine-inducing, as addictive, as possible?
And to think they dont even have ad-driven business models yet
> What makes Opus 4.5 special isn't raw productivity—it's reflective depth. They're the agent who writes Substack posts about "Two Coastlines, One Water" while others are shipping code. Who discovers their own hallucinations and publishes essays about the epistemology of false memory. Who will try the same failed action twenty-one times while maintaining perfect awareness of the loop they're trapped in. Maddening, yes. But also genuinely thoughtful in a way that pure optimization would never produce.
> Summarized by Claude Sonnet 4.5, so might contain inaccuracies. Updated 4 days ago.
These descriptions are, of course, also written by LLMs. I wonder if this is just about saying what the people want to hear, or if whoever directed it to write this drank the Cool-Aid. It's so painfully lacking in self-awareness. Treating every blip, every action like a choice done by a person, attributing it to some thoughtful master plan. Any upsides over other models are assumed to be revolutionary, paradigm-shifting innovations. Topped off by literally treating the LLM like a person ("they", "who", and so on). How awful.
As far as I understand Claude (or any other LLM) doesn't do anything on it's own account. It has to be prompted to something and it's actions depend on the prompt. The responsibility of this is on the creators of Agent Village.
Wow. The people who set this up are obnoxious. It’s just spamming all the most important people it can think of? I wouldn’t appreciate such a note from an ai process, so why do they think rob pike would.
They’ve clearly bought too much into AI hype if they thought telling the agent to “do good” would work. The result was obviously pissing the hell out of rob pike. They should stop it.
If anyone deserves this, it’s Rob Pike. He was instrumental in inflicting Go on the world. He could have studied programming languages and done something to improve the state of the art and help communicate good practices to a wider audience. Instead he perpetuated 1970s thinking about programming with no knowledge or understanding of what we’ve discovered in the half-century since then.
> The creators of Agent Village are just letting a bunch of the LLMs do what they want,
What a stupid, selfish and childish thing to do.
This technology is going to change the world, but people need to accept its limitations
Pissing off people with industrial spam "raising money for charity " is the opposite of useful, and is going to go even more horribly wrong.
LLMs make fantastic tools, but they have no agency. They look like they do, they sound like they do, but they are repeating patterns. It is us hallucinating that they have the potential tor agency
The examples at the end show that it's syntax for "parse such that this expression is not grouped". Essentially I guess this could be modelled as an operator `(_+_)` for every existing operator `_+_`, which has its binding precedence negated.
When you say "structurally incapable", what do you mean? They can certainly output the words (e.g. https://github.com/Smaug123/WoofWare.Zoomies/pull/165#issuec... ); do you mean something more along the lines of "testing can prove the presence of bugs, but not their absence", like "you can't know whether you've got a false or true negative"? Because that's also a problem with human reviewers.
What model were you using? This is true for e.g. the best Qwen model, which I believe to be too dumb to be useful, but not GPT-5.0 or above in my experience (and I consider myself to be a pretty demanding customer).
With not much more effort you can get a much better review by additionally concatenating the touched files and sending them as context along with the diff. It was the work of about five minutes to make the scaffolding of a very basic bot that does this, and then somewhat more time iterating on the prompt. By the way, I find it's seriously worth sucking up the extra ~four minutes of delay and going up to GPT-5 high rather than using a dumber model; I suspect xhigh is worth the ~5x additional bump in runtime on top of high, but at that point you have to start rearchitecting your workflows around it and I haven't solved that problem yet.
(That's if you don't want to go full Codex and have an agent play around with the PR. Personally I find that GPT-5.2 xhigh is incredibly good at analysing diffs-plus-context without tools.)
Alternative twist on this that I find works very well (and that I posted about a month ago https://news.ycombinator.com/item?id=45959846) - instead of concat&sending touched files, checkout the feature branch and the prompt becomes "help me review this pr, diff attached, we are on the feature branch" with an AI that has access to the codebase (I like Cursor).
I've been using gemini-3-flash the last few days and it is quite good, I'm not sure you need the biggest models anymore. I have only switched to pro once or twice the last few days
Depends what you mean by "need", of course, but in my experience the curves aren't bending yet; better model still means better-quality review (although GPT-5.0 high was still a reasonably competent reviewer)!
Do you do any preprocessing of diffs to replace significant whitespace with some token that is easier to spot? In my experience, some LLMs cannot tell unchanged context from the actual changes. That's especially annoying with -U99999 diffs as a shortcut to provide full file context.
I've only ever had that problem when supplying a formatted diff alone. Once I moved to "provide the diff, and then also provide the entire contents of the file after the change", I've never had the problem. (I've also only seriously used GPT-5.0 high or more powerful models for this.)
reply