wizzwizz4

However, I couldn't care less about the feelings of chatbots. What I do care about is the feelings of the people to whom the slurs were originally directed, and (generally) the kind of culture that this creates. The use of slurs is a symptom, rather than a cause, but complaining about slurs does get people asking the kinds of questions you're asking, which is a positive.

I would not have said anything if the word "clanker", alone, had been used. But if you look at GP's other comments, I think you'll see evidence to support my musings about the kind of attitude that the practice of slur use cultivates.

  <noob> Where do birds go when it rains?
  <expert> They

Or friction.

If you were using Isabelle/HOL, then (depending on field) you could already have had this. Sledgehammer is pretty powerful, even though it's "just"¹ SAT solvers plus (not-quite-naïve) brute-force. Writes awful proofs (even if half a minute of staring reveals elegant concepts behind it), and can take a very long time to run if you don't have sensible intermediate lemmas (although you'll be writing those anyway, in the course of your work), but if you start at the top of the page and work down, writing "try" in place of every proof, you'll get proofs (or counterexamples) of nearly everything, without putting in any extra work. (This is pre-LLM technology, to be clear: they just have a terrible marketing department.)

There's currently a UI issue where you have to accept the proofs in reverse order (bottom to top), otherwise it goes "oh, something changed!" and wipes the attempts it was making for the later proofs; but that shouldn't be too hard to fix with a non-local cache – and in the meantime, it's quite a minor quirk. On a researcher's laptop (i.e., one considerably more powerful than mine!), it's rare that sledgehammer finds a proof slower than it takes to type out the statement of the next theorem, and the "try" keyword changes background colour to let you know when it's done.

You'll notice I said "sensible intermediate lemmas". You might need to recalibrate your notion of elegance slightly for this, if you want to get fast proofs out the other end – but sledgehammer can work with even totally backwards lemmas like "∀list. list = hd list ## tl list": it'll just use a general-purpose solver rather than a special-purpose one, and so be a lot slower to find proofs. In practice, this is not an issue: it's an easier, more explicable skill than prompt engineering, and Isabelle will mostly just work around you if you do it wrong.

> if you need a particular prerequisite theorem from the end of a textbook, you'd rather do it faster than half the reading speed (that's impressive by the way, […])

Note that this is my mathematics reading speed, not my English reading speed. It might not be as impressive as you think. The number of times I've had to go back and re-read four pages because I misunderstood a basic concept…

Well, if I were formalising for the sake of assisting my research, rather than for the joy of formalisation (which, honestly, isn't all that: Isabelle's better than Lean, but it's far from nice), and I just needed a result from the end of a textbook, I'd be very tempted to write:

  theorem final_theorem: ‹statement of theorem›
    sorry  ― ‹TODO: Proven in textbook reference, page 189.›

One thing to note: if this theorem isn't true, then Sledgehammer is prone to helpfully exploiting the principle of explosion to prove everything else for you, even other things that are not true. You can usually spot this at a glance, if it's dragging in unrelated theorems.

> I'd also like to claim that the elegance of arguments is probably at least as important as the elegance of definitions. And if you find an elegant argument, later on that might serve as a basis of a definition.

Yup! And sometimes different arguments motivate different definitions, and then you end up with a graph of "definition A is easier to prove from definition B than the other way around", which either resolves into a "definition I is the best weak definition for introduction, and definition D is the best strong definition for destruction/elimination", or a circle of equally-valid definitions. (Sadly, I've only encountered the latter in textbooks: never in my own research, however often I've believed I have. But I'm holding out hope!)

> I think LLMs are a bit better with arguments than definitions

So's Isabelle's sledgehammer. Try it? (Again, depending on which field you work in: some things just aren't formalised at all in Isabelle/HOL, so you can't really use them, although a surprising amount is. Given more information, I can give better advice.)

> (Hmm, a random idle thought, but a refactor from arguments to specific theorems could be in some sense similar as going from an untyped or not-explicitly-typed programming language to a typed one so there might be a coding analogue here as well.)

Yeah, we call that category theory. The big downside of Isabelle/HOL is that it can't do category theory, because it can't quantify over types: each "argument" has to be written out explicitly, generic over a large (usually infinite) family of use-cases, but not all of them in the way that a dependently-typed logic like Lean can.

But this limitation does make the automation more powerful, so that's actually a good thing for your use-case. I don't understand enough to know how it makes it more powerful, but I imagine it's something like "narrowing the search lets you search deeper". Lean's (currently, and perhaps inherently, inferior) version of sledgehammer has a module that tries to translate Lean expressions into HOL expressions, so it can use some of the techniques available to Isabelle/HOL's sledgehammer. (Some of the Isabelle people have joked that instead of using LLMs, Lean should just bundle a copy of Isabelle/HOL – and while obviously this wouldn't work, it might genuinely work better than LLMs for most use-cases.)

> I also feel that LLMs are probably not currently able to really go beyond their training data, […] They are getting very good at combining and rephrasing existing stuff, however.

I'm concerned that this will lead to increased plagiarism. When Isabelle finds a proof, it tells you where it got it. (That's actually how I learned about the Cantor–Schröder–Bernstein theorem, which finally convinced me that what I was trying to prove was independent of ZF: it told me the name of this theorem, when solving a problem that I didn't think was deeply related to the axiom of choice. All pre-LLM technology, mind! And it'd have done exactly the same for a lesser-known theorem, provided that the theorem was known to Isabelle.) LLMs (usually (when they succeed)) give you answers, and then do a post-hoc search for where the answers might have come from.

¹: The scare quotes around "just" are doing a lot of heavy lifting. Jasmin Blanchette is a clear communicator, so most Sledgehammer articles are accessible to non-experts: you may find Sledgehammering Without ATPs (https://doi.org/10.4230/LIPIcs.ITP.2025.38) or Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL (https://arxiv.org/abs/2508.20738) interesting reading. Or Redirecting Proofs by Contradiction (https://isabelle.in.tum.de/~blanchet/redirect.pdf), which describes a much older version of Sledgehammer and is rather technically-dense, but has some interesting observations about human versus computer mathematics.

Not in any aspect comparable to a Nazi. Gotcha. Hey, out of interest, have you read Mein Kampf, by Adolf Hitler? Here's a bit of Ludwig Lore's translation, Chapter 2:

> The great mass of people could be saved, even if only by the utmost sacrifice of time and patience. But no Jew could ever be freed from his opinion.

(I'm not sure whether you're seriously arguing that bloggers have the capacity to construct offshore death camps to which they deport "undesirables", or the power to unilaterally and militarily invade Poland, and the fact they haven't done so reflects well upon their characters; so I'll not attempt to refute that point until it is clarified.)

Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.)

> Granted their goal was not so much speed as it was elegance,

Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit.

¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough. "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)

I see no mention of the far right in Taylor Lorenz's article. I do see mentions of Donald Trump, DOGE, and the Republican party in the NYT article cited in the "Politics" section. As I understand, these entities are considered "right-wing" in US terms, and many of their actions would certainly be considered "extreme". ("Extreme" is somewhat subjective, so for the sake of foreshortening this argument, I'll set it at the objective threshold of ten thousand dead children.)

> "The Tech Right […]", but this is only being used to cite Boyle

So, you found a source describing Katherine Boyle, in her capacity as manager of Andreessen Horowitz's American Dynamism fund, as right-wing. This seems to support Taylor Lorenz's claim.

> but even so I don't see what's extreme about anything attributed to [Marc Andreessen] in his own article.

Aside from working for DOGE, and strongly supporting cryptocurrency and AI, I would agree with your expectation that a large percentage of Americans would find his views agreeable: I would expect slightly under half the US population. These views are not so popular internationally.

As a reminder: I would rather not debate this here. TFA is an article about Substack, not Andreessen Horowitz's political leanings: we should be discussing Substack, not its investor.

> FWIW, I consider that the actual literal Nazis were a step beyond typical contemporary American white supremacists.

To start with, the Nazis were much, much tamer. For example, the Nazis neither owned, whipped, nor branded people in 1924, whereas the second KKK had only just started to fracture at that point. It was only once the Nazis got control of the state apparatus that they got really bad: the Night of Broken Glass, Aktion T4, the invasion of Poland, the Holocaust…. Adolf Hitler (claimed to have) modelled parts of the Nazi regime on American white supremacist practices.

The Nazi party started with the recruitment of Nazis. By the time they were an organised fascist paramilitary capable of attempting a coup (1922–1923), it was almost too late to stop them.

> Note that the headline of your own source explicitly describes Substack as having offered an apology,

A qualified apology, of the form: "We're sorry if our policies lead to the systematic platforming of white supremacist hatemongers, and of course the active promotion of this neo-Nazi organisation by our computer systems was a one-off mistake, but we won't change our policies: if we don't give Nazis a voice, then they'll say even worse things!" That's not really an apology: it's a "we're sorry for the bad press we're experiencing".

Also, PayPal's fee, as described, is fairly steep:

> PayPal charges a base fee of 30 cents and 2.9% of the donation amount within Canada. There's an additional 0.8% fee for donations from the US and 1% for other countries. Currency conversion adds an additional 4% fee as opposed to the usual PayPal conversion fee of 3%.

One of the first newsy types to report this particular issue, but certainly not the only one. See https://arstechnica.com/tech-policy/2025/07/substacks-nazi-p..., which quotes a press release from Substack. Arguably, my source is therefore Substack themselves, via Ars Technica.

> Something which Wikipedia editors would be tripping over each other to evidence if it were true, but their article says nothing about it.

Actually, this information is on Wikipedia. There's one NYT link on the Andreessen Horowitz article, and several paragraphs on Marc Andreessen's. I don't know enough about US politics to know whether all this adds up to "extreme far right rhetoric" (and I'd rather not debate that here), but there's definitely extreme, and right-wing, political advocacy described in Marc Andreessen's article. I have not confirmed whether the claims in the Wikipedia article are correct; if you dispute them, then please let me know as a courtesy (I like having accurate knowledge), then take it up with the Wikipedia editors.

> There is nothing to demonstrate the claim that Substack "continues, proudly" to host such content,

But they do continue to host it. This has been a problem for years (see e.g. https://www.theatlantic.com/ideas/archive/2023/11/substack-e..., https://www.theguardian.com/media/2026/feb/07/revealed-how-s...). Do you need an article from last month? Or do I need to link you to a Nazi blog directly? They are not very hard to find: just type "site:substack.com" followed by some keywords. It took me 20 seconds to find one called "White Free Press", with such wonderful articles as "David Lane and the Foundations of His Racial Ideology", "The Contemporary Conceptual Framework of the White Ethnostate", and "The Immutable Animosity: blacts [sic] hate White People, and Nothing Can Change It".

> It is a known tactic of agitators […]

Quoting the Ars Technica article:

> Of those accounts created in February, only the Substack account is still online, which Fisher-Birch suggested likely sends a message to Nazi groups that their Substack content is “less likely to be removed than other platforms.” At least one Terrorgram-adjacent white supremacist account that Fisher-Birch found in March 2024 confirmed that Substack was viewed as a back-up to Telegram because it was that much more reliable to post content there.

> “Groups that want to recruit members or build a neo-fascist counter-culture see Substack as a way to get their message out,” Fisher-Birch told Ars.

I don't think "this is all some kind of contrived false flag operation" is a particularly likely explanation.

> Substack sent a push alert encouraging users to subscribe to a Nazi newsletter that claimed Jewish people are a sickness and that we must eradicate minorities to build a “White homeland.” […] The newsletter's logo is a swastika and it has pushed Holocaust denialism along with news and opinion content for the 'White Nationalist Community.' […] Substack is primarily funded by Andreessen Horowitz, a firm whose founders have pushed extreme far right rhetoric.

If AI causes people to kill who otherwise wouldn't have, I expect it to be by causing and exacerbating mental health problems, not by providing knowledge. (See e.g. https://www.bbc.co.uk/news/technology-67012224, where a roleplay escalated into a concrete plan to kill Queen Elizabeth II over the course of two weeks. The plan wasn't, however, a very good one.)

You're probably thinking of geometrical super-resolution, such as gigapixel photography. Blurring is the discarding of high-frequency information, and only a very very small part of this information can be recovered using techniques like this (as in, so little that you wouldn't be able to notice it).

> My only point is information in a video is more than the sum of the information of it's frames,

It's actually less than the sum of the information of it's frames. An off-the-shelf lossless compression algorithm can give you an upper bound for the amount of information present in a video file.