One important nuance is that there are, broadly speaking, two ways to express a formal proof: it can either be fairly small but take exponential time to verify, or it can be fairly quick to verify but exponentially large. Most folks prefer to use the former sort of system. However, with extension by definitions, we can have a polynomial number of polynomially-large definitions while still verifying quickly. This leads to my favorite proof system, Metamath, whose implementations measure their verification speed in kiloproofs/second. If you give me a Metamath database then I can quickly confirm any statement in a few moments with multiple programs and there is programmatic support for looking up the axioms associated with any statement; I can throw more compute at the problem. While LLMs do know how to generate valid-looking Metamath in context, it’s safe to try to verify their proofs because Metamath’s kernel is literally one (1) string-handling rule.

This is all to reconfirm your impression that e.g. Lean inherits a “mediocre software engineering” approach. Junk theorems in Lean are laughably bad due to type coercions. The wider world of HOL is more concerned with piles of lambda calculus than with writing math proofs. Lean as a general-purpose language with I/O means that it is no longer safe to verify untrusted proofs, which makes proof-carrying Lean programs unsafe in practice.

@Seminar2250@awful.systems you might get a laugh out of this too. FWIW I went in the other direction: I started out as a musician who learned to code for dayjob and now I’m a logician.

I don’t have any good lay literature, but get ready for “steering vectors” this year. It seems like two or three different research groups (depending on whether I count as a research group) independently discovered them over the past two years and they are very effective at guardrailing because they can e.g. make slurs unutterable without compromising reasoning. If you’re willing to read whitepapers, try Dunefsky & Cohan, 2024 which builds that example into a complete workflow or Konen et al, 2024 which considers steering as an instance of style transfer.

I do wonder, in the engineering-disaster-podcast sense, exactly what went wrong at OpenAI because they aren’t part of this line of research. HuggingFace is up-to-date on the state of the art; they have a GH repo and a video tutorial on how to steer LLaMA. Meanwhile, if you’ll let me be Bayesian for a moment, my current estimate is that OpenAI will not add steering vectors to their products this year; they’re already doing something like it internally, but the customer-facing version will not be ready until 2027. They just aren’t keeping up with research!

Steve Yegge has created Gas Town, a mess of Claude Code agents forced to cosplay as a k8s cluster with a Mad Max theme. I can’t think of better sneers than Yegge’s own commentary:

Gas Town is also expensive as hell. You won’t like Gas Town if you ever have to think, even for a moment, about where money comes from. I had to get my second Claude Code account, finally; they don’t let you siphon unlimited dollars from a single account, so you need multiple emails and siphons, it’s all very silly. My calculations show that now that Gas Town has finally achieved liftoff, I will need a third Claude Code account by the end of next week. It is a cash guzzler.

If you’re familiar with the Towers-of-Hanoi problem then you can appreciate the contrast between Yegge’s solution and a standard solution; in general, recursive solutions are fewer than ten lines of code.

Gas Town solves the MAKER problem (20-disc Hanoi towers) trivially with a million-step wisp you can generate from a formula. I ran the 10-disc one last night for fun in a few minutes, just to prove a thousand steps was no issue (MAKER paper says LLMs fail after a few hundred). The 20-disc wisp would take about 30 hours.

For comparison, solving for 20 discs in the famously-slow CPython programming system takes less than a second, with most time spent printing lines to the console. The solution length is exponential in the number of discs, and that’s over one million lines total. At thirty hours, Yegge’s harness solves Hanoi at fewer than ten lines/second! Also I can’t help but notice that he didn’t verify the correctness of the solution; by “run” he means that he got an LLM to print out a solution-shaped line.

NEOM is a laundry for money, religion, genocidal displacement, and the Saudi reputation among Muslims. NEOM is meant to replace Wahhabism, the Saudi family’s uniquely violent fundamentalism, with a much more watered-down secularist vision of the House of Saud where the monarchs are generous with money, kind to women, and righteously uphold their obligations as keepers of Mecca. NEOM is not only The Line, the mirrored city; it is multiple different projects, each set up with the Potemkin-village pattern to assure investors that the money is not being misspent. In each project, the House of Saud has targeted various nomads and minority tribes, displacing indigenous peoples who are inconvenient for the Saudi ethnostate, with the excuse that those tribes are squatting on holy land which NEOM’s shrines will further glorify.

They want you to look at the smoke and mirrors in the desert because otherwise you might see the blood of refugees and the bones of the indigenous. A racing team is one of the cheaper distractions.

I clicked through too much and ended up finding this. Congrats to jdp for getting onto my radar, I suppose. Are LLMs bad for humans? Maybe. Are LLMs secretly creating a (mind-)virus without telling humans? That’s a helluva question, you should share your drugs with me while we talk about it.

Nah, it’s more to do with stationary distributions. Most tokens tend to move towards it; only very surprising tokens can move away. (Insert physics metaphor here.) Most LLM architectures are Markov, so once they get near that distribution they cannot escape on their own. There can easily be hundreds of thousands of orbits near the stationary distribution, each fixated on a simple token sequence and unable to deviate. Moreover, since most LLM architectures have some sort of meta-learning (e.g. attention) they can simulate situations where part of a simulation can get stuck while the rest of it continues, e.g. only one chat participant is stationary and the others are not.

Upvoted, but also consider: boycotts sometimes work. BDS is sufficiently effective that there are retaliatory laws against BDS.

Other classic Rob Pike moments include spamming Usenet with Markov-chain bots and quoting the Bible to justify not highlighting Go syntax. Watching him have a Biblical meltdown over somebody emailing him generated text is incredibly funny in this context.

It’s a power play. Engineers know that they’re valuable enough that they can organize openly; also, as in the case of Alphabet Workers Union, engineers can act in solidarity with contractors, temps, and interns. I’ve personally done things like directly emailing CEOs with reply-all, interrupting all-hands to correct upper management on the law, and other fun stuff. One does have to be sufficiently skilled and competent to invoke the Steve Martin principle: “be so good that they can’t ignore you.”

It might help to know that Paul Frazee, one of the BlueSky developers, doesn’t understand capability theory or how hackers approach a computer. They believe that anything hidden by the porcelain/high-level UI is hidden for good. This was a problem on their Beaker project, too; they thought that a page was deleted if it didn’t show up in the browser. They fundamentally aren’t prepared for the fact that their AT protocol doesn’t have a way to destroy or hide data and is embedded into a network that treats censorship as reparable damage.

Today, in fascists not understanding art, a suckless fascist praised Mozilla’s 1998 branding:

This is real art; in stark contrast to the brutalist, generic mess that the Mozilla logo has become. Open source projects should be more daring with their visual communications.

Quoting from a 2016 explainer:

[T]he branding strategy I chose for our project was based on propaganda-themed art in a Constructivist / Futurist style highly reminiscent of Soviet propaganda posters. And then when people complained about that, I explained in detail that Futurism was a popular style of propaganda art on all sides of the early 20th century conflicts… Yes, I absolutely branded Mozilla.org that way for the subtext of “these free software people are all a bunch of commies.” I was trolling. I trolled them so hard.

The irony of a suckless developer complaining about brutalism is truly remarkable; these fuckwits don’t actually have a sense of art history, only what looks cool to them. Big lizard, hard-to-read font, edgy angular corners, and red-and-black palette are all cool symbols to the teenage boy’s mind, and the fascist never really grows out of that mindset.

Sadly, it’s a Chomskian paper, and those are just too weak for today. Also, I think it’s sloppy and too Eurocentric. Here are some of the biggest gaffes or stretches I found by skimming Moro’s $30 book, which I obtained by asking a shadow library for “impossible languages” (ISBN doesn’t work for some reason):

I think that Moro’s strongest point, on which they spend an entire chapter reviewing fairly solid neuroscience, is that natural language is spoken and heard, such that a proper language model must be simultaneously acoustic and textual. But because they don’t address computability theory at all, they completely fail to address the modern critique that machines can learn any learnable system, including grammars; they worst that they can say is that it’s literally not a human.

I got jumpscared by Gavin D. Howard today; apparently his version of bc appeared on my system somehow, and his name’s in the copyright notice. Who is Gavin anyway? Well, he used to have a blog post that straight-up admitted his fascism, but I can’t find it. I could only find, say, the following five articles, presented chronologically:

• Free Speech and Pronouns
• Israel is Not an Apartheid State, featuring Denis “No U” Prager
• My Thought Process Regarding Vaccines
• Intermission: This comment on Lobsters leads to this ban reason on Lobsters
• No More Skittles, featuring Libs of “TikTok” TikTok
• I Am Divorced

Also, while he’s apparently not caused issues for NixOS maintainers yet, he’s written An Apology to the Gentoo Authors for not following their rules when it comes to that same bc package. So this might be worth removing for other reasons than the Christofascist authorship.

BTW his code shows up because it’s in upstream BusyBox and I have a BusyBox on my system for emergency purposes. I suppose it’s time to look at whether there is a better BusyBox out there. Also, it looks like Denys Vlasenko has made over one hundred edits to this code to integrate it with BusyBox, fix correctness and safety bugs, and improve performance; Gavin only made the initial commit.

They (or the LLM that summarized their findings and may have hallucinated part of the post) say:

It is a fascinating example of “Glue Code” engineering, but it debunks the idea that the LLM is natively “understanding” or manipulating files. It’s just pushing buttons on a very complex, very human-made machine.

Literally nothing that they show here is bad software engineering. It sounds like they expected that the LLM’s internals would be 100% token-driven inference-oriented programming, or perhaps a mix of that and vibe code, and they are disappointed that it’s merely a standard Silicon Valley cloudy product.

My analysis is that Bobby and Vicky should get raises; they aren’t paid enough for this bullshit.

By the way, the post probably isn’t faked. Google-internal go/ URLs do leak out sometimes, usually in comments. Searching GitHub for that specific URL turns up one hit in a repository which claims to hold a partial dump of the OpenAI agents. Here is combined_apply_patch_cli.py. The agent includes a copy of ImageMagick; truly, ImageMagick is our ecosystem’s cockroach.

Now I’m curious about whether Disney funded Glaze & Nightshade. Quoting Nightshade’s FAQ, their lab has arranged to receive donations which are washed through the University of Chicago:

If you or your organization may be interested in pitching in to support and advance our work, you can donate directly to Glaze via the Physical Sciences Division webpage, click on “Make a gift to PSD” and choose “GLAZE” as your area of support (managed by the University of Chicago Physical Sciences Division).

Previously, on Awful, I noted the issues with Nightshade and the curious fact that Disney is the only example stakeholder named in the original Nightshade paper, as well as the fact that Nightshade’s authors wonder about the possibility of applying Glaze-style techniques to feature-length films.

The author also proposes a framework for analyzing claims about generative AI. I don’t know if I endorse it fully, but I agree that each of the four talking points represents a massive failure of understanding. Their LIES model is:

• Lethality: the bots will kill us all
• Inevitability: the bots are unstoppable and will definitely be created in the future
• Exceptionalism: the bots are wholly unlike any past technology and we are unprepared to understand them
• Superintelligent: the bots are better than people at thinking

I would add to this a Plausibility or Personhood or Personality: the incorrect claim that the bots are people. Maybe call it PILES.

Fundamentally, Chapman’s essay is about how subcultures transition from valuing functionality to aesthetics. Subcultures start with form following function by necessity. However, people adopt the subculture because they like the surface appearance of those forms, leading to the subculture eventually hollowing out into a system which follows the iron law of bureaucracy and becomes non-functional due to over-investment in the façade and tearing down of Chesterton’s fences. Chapman’s not the only person to notice this pattern; other instances of it, running the spectrum from right to left, include:

• Rao’s The Gervais Principle, which Chapman explicitly cites, is about how businesses operate
• Baudrillard’s Simulacra and Simulation is about how semiotic systems evolve
• Benjamin’s The Work of Art in the Age of Mechanical Reproduction is about how groups of artists establish symbols
• Debord’s The Society of the Spectacle is about how consumerist states cultivate mass consciousness through mass media
• The Marxist concept that fascism is a cancer upon liberalism, which doesn’t have a single author as far as I can tell, is about how political systems evolve under obligate capitalism

I think that seeing this pattern is fine, but worrying about it makes one into Scott Alexander, paranoid about societal manipulation and constantly worrying about in-group and out-group status. We should note the pattern but stop endorsing instances of it which attach labels to people; after all, the pattern’s fundamentally about memes, not humans.

So, on Chapman. I think that they’re a self-important nerd who reached criticality after binge-reading philsophy texts in graduate school. I could have sworn that this was accompanied by psychedelic drugs, but I can’t confirm or cite that and I don’t think that we should underestimate the psychoactive effect of reading philosophy from the 1800s. In his own words:

[T]he central character in the book is a student at the MIT Artificial Intelligence Laboratory who discovers Continental philosophy and social theory, realizes that AI is on a fundamentally wrong track, and sets about reforming the field to incorporate those other viewpoints. That describes precisely two people in the real world: me, and my sometime-collaborator Phil Agre.

He’s explicitly not allied with our good friends, but at the same time they move in the same intellectual circles. I’m familiar with that sort of frustration. Like, he rejects neoreaction by citing Scott Alexander’s rejection of neoreaction (source); that’s a somewhat-incoherent view suggesting that he’s politically naïve. His glossary for his eternally-unfinished Continental-style tome contains the following statement on Rationalism (embedded links and formatting removed):

Rationalisms are ideologies that claim that there is some way of thinking that is the correct one, and you should always use it. Some rationalisms specifically identify which method is right and why. Others merely suppose there must be a single correct way to think, but admit we don’t know quite what it is; or they extol a vague principle like “the scientific method.” Rationalism is not the same thing as rationality, which refers to a nebulous collection of more-or-less formal ways of thinking and acting that work well for particular purposes in particular sorts of contexts.

I don’t know. Sometimes he takes Yudkowsky seriously in order to critique him. (source, source) But the critiques are always very polite, no sneering. Maybe he’s really that sort of Alan Watts character who has transcended petty squabbles. Maybe he didn’t take enough LSD. I once was on LSD when I was at the office working all day; I saw the entire structure of the corporation, fully understood its purpose, and — unlike Chapman, apparently — came to the conclusion that it is bad. Similarly, when I look at Yudkowsky or Yarvin trying to do philosophy, I often see bad arguments and premises. Being judgemental here is kind of important for defending ourselves from a very real alt-right snowstorm of mystic bullshit.

Okay, so in addition to the opening possibilities of being naïve and hiding his power level, I suggest that Chapman could be totally at peace or permanently rotated in five dimensions from drugs. I’ve gotta do five, so a fifth possibility is that he’s not writing for a human audience, but aiming to be crawled by LLM data-scrapers. Food for thought for this community: if you say something pseudo-profound near LessWrong then it is likely to be incorporated into LLM training data. I know of multiple other writers deliberately doing this sort of thing.

The orange-site whippersnappers don’t realize how old artificial neurons are. In terms of theory, the Hebbian principle was documented in 1949 and the perceptron was proposed in 1943 in an article with the delightfully-dated name, “A logical calculus of the ideas immanent in nervous activity”. In 1957, the Mark I Perceptron was introduced; in modern parlance, it was a configurable image classifier with a single layer of hundreds-to-thousands of neurons and a square grid of dozens-to-hundreds of pixels. For comparison, MIT’s AI lab was founded in 1970. RMS would have read about artificial neurons as part of their classwork and research, although it wasn’t part of MIT’s AI programme.

Oh wow, that’s gloriously terse. I agree that it might be the shortest. For comparison, here are three other policies whose pages are much longer and whose message also boils down to “don’t do that”: don’t post copypasta, don’t start hoaxes, don’t start any horseshit either.

Ziz was arraigned on Monday, according to The Baltimore Banner. She apparently was not very cooperative:

As the judge asked basic questions such as whether she had read the indictment and understood the maximum possible penalties, [Ziz] LaSota chided the “mock proceedings” and said [US Magistrate Douglas R.] Miller was a “participant in an organized crime ring” led by the “states united in slavery.”

She pulled the Old Man from Scene 24 gag:

Please state your name for the record, the court clerk said. “Justice,” she replied. What is your age? “Timeless.” What year were you born? “I have been born many times.”

The lawyers have accepted that sometimes a defendant is uncooperative:

Prosecutors said the federal case would take about three days to try. Defense attorney Gary Proctor, in an apparent nod to how long what should have been a perfunctory appearance on Monday ended up taking, called the estimate “overly optimistic.”

Folks outside the USA should be reassured that this isn’t the first time that we’ve tried somebody with a loose grasp of reality and a found family of young violent women who constantly disrupt the trial; Ziz isn’t likely to walk away.