Have a sneer percolating in your system but not enough time/energy to make a whole post about it? Go forth and be mid - welcome to the Stubsack, your first port of call for learning fresh Awful you’ll near-instantly regret.
Any awful.systems sub may be subsneered in this subthread, techtakes or no.
If your sneer seems higher quality than you thought, feel free to cut’n’paste it into its own post — there’s no quota for posting and the bar really isn’t that high.
The post Xitter web has spawned so many “esoteric” right wing freaks, but there’s no appropriate sneer-space for them. I’m talking redscare-ish, reality challenged “culture critics” who write about everything but understand nothing. I’m talking about reply-guys who make the same 6 tweets about the same 3 subjects. They’re inescapable at this point, yet I don’t see them mocked (as much as they should be)
Like, there was one dude a while back who insisted that women couldn’t be surgeons because they didn’t believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I can’t escape them, I would love to sneer at them.
(Credit and/or blame to David Gerard - both for starting this, and for covering the previous week. We should get a bot to automate this…)
Aella took one of her shitty twitter surveys and made an (dis)infographic, which made it onto the subreddit /r/moralityscaling, which made it to /r/whowouldcirclejerk where I saw it, so now I’m sharing it with you.
CW for Rape, Transphobia, implicit rape apologia
Crossposted from our subreddit: https://www.reddit.com/r/SneerClub/comments/1v80j9q/scalers_need_an_intervention/
That link is login-walled, how about summarizing it?
Oh, that is because I marked it nsfw. The place I crossposted it from didn’t mark it as such, so here’s that link: https://www.reddit.com/r/whowouldcirclejerk/comments/1v7ph05/scalers_need_an_intervention/
The controversy about the 26-year-old with the 16-year-old wonders if the respondents are all in California which has a very high age of consent. More replies say that is rape than say “a client fails to pay a sex worker” is rape. Her audience ranks it equally with the bodice-ripper scenario (handsome top ravages someone who says no and struggles but really wants it in his or her heart).
Tennessee here: what the chicken-fried fuck is wrong with these people?
I think we’re watching some idiots who are trying to move the overton widow by pulling on it, but they’re mostly succeeding at cutting their hands up really badly.
I’ve think they’ve moved the overton window within their own in-group, but whenever this sort of stuff leaks to a more mainstream audience everyone rightly reacts with an eww or at least a wtf.
As the post was removed: It was a chart of what rape percentage various situations were according to some internet survey.
I advise not reading it but here it is: https://pbs.twimg.com/media/G41gJkzW4AA6ThU.jpg?name=orig
There is some pedophilia in there too.
…also, what the fuck. This is a step backwards, even just reading it. I’m mad.
[Removed by Moderator]
Ah, that’s probably better for my mental health I guess
Jesus fucking christ none of these people should be having sex
never thought id see r/moralityscaling and r/whowouldcirclejerk here ever lol. but christ alive why would you ever conceive of this
Who spends time thinking about this? What purpose does it serve? Why are those the examples chosen? What is even going on?
Aella regularly post edgy surveys on sexual and gender related topics on twitter. She probably picked the examples for maximum edginess. And then made an complicated diagram to get more engagement, because engagement farming is one of her big things.
A LWer runs the numbers and doesn’t run away screaming like Zitron:
https://www.lesswrong.com/posts/EeTQGxa8RSpwHo4Ez/the-biggest-bet-in-history
Note that this implies massive efficiency gains to the economy. For their one-third slice to equal 8% of those salaries [59% of the total workforce in the USA], the total savings (productivity across that share of the workforce) will need to rise by roughly 24%. So they are absolutely serious about this, and are betting heavily that the productivity boost arrives within four years.
Guys guys guys hear me out guys what if I say what if uh the market can’t be irrational? Because of all the money? That would be really cool right?
But using like 2000 words.
“surely all these very wealthy people and the people they pay to invest for them can’t all be under some sort of mass delusion”
(there’s actually one other dynamic, in which they all know someone will lose, and are just hoping it isn’t them, but that’s another post)
Uh huh.
Sure sounds like aspiring and/or existing professional mathematicians are taking the latest GenAI assault on their craft either with shock or horror, or with full-on welcoming of their new robot overlords
https://borretti.me/article/mathematics-without-mathematicians
I for one know who to point and laugh at when the revolution comes.
Clamuel did another podcast. I don’t want to waste my time watching it, but I want to sneer at some choice quotes from news articles breathlessly reporting this stuff as gospel 1, 2
“We are now, like, in the singularity”
Is the singularity in the room with us right now? Even the people on X the Everything (Including CSAM) App aren’t so convinced.
Altman said on the podcast that just a decade ago, the so-called singularity still felt like a distant and improbable dream — something he and his colleagues would discuss casually over lunch.
“Now we’re actually in the moment that we used to talk about at the lunch table in a very not-serious way,” he said. “I’ve been waiting for this my whole life, and I think it’s going to be incredible, hugely positive, awesome for the world.”
Do you feel it? Do you feel incredible? Do you feel hugely positive? Do you feel awesome, now that the singularity is here? Oh wait, he’s speaking in the future tense again, never mind. Force of habit.
It’s also funny how he talks about how positive things are gonna be immediately after the super scary hack done on Hugging Face (really due to incompetence on both sides). Oh no, the AI is gonna kill us all! It’s going to be incredible, hugely positive, awesome for the world.
Later in the podcast, Altman criticizes AI leaders who have repeatedly warned that AI is dangerous. He didn’t name Anthropic, his primary competition, but its CEO, Dario Amodei, is well-known for making dire predictions about the future in his calls for greater attention to safety.
“I also think some of the alternative visions painted by other companies are quite terrifying,” Altman said. “I’m going to make sure that gets pushed against and is not what happens.”
At least Clammy realizes that all the doom trolling about how AI will replace and destroy all humans turns out, surprisingly, to lead to overwhelming negative public opinion. But this statement truly reassures me that Scammy has good intentions about AI safety. He will make sure this is pushed against and is not what happens. He wouldn’t want another super scary, dangerous hack that just so conveniently turns out to be excellent marketing.
OpenAI CEO Sam Altman says one of his biggest concerns about AI isn’t whether it becomes too powerful in and of itself, but that a single company could control that power.
Yeah, it would be really bad for Anthropic to control all the power of AI. It would be a disaster to hand everything over to Anthropic.
“Every time that humanity has traded off its liberty for safety, it’s been a long-term net loss,” Altman said. “We are going to put this in the hands of people. We’re going to empower them. We are going to let society express its ideas and use this technology in the way they want.”
Society is expressing its ideas about AI, all right. But I feel like they aren’t what he has in mind.
Altman, meanwhile, said preventing such power from becoming overly concentrated has long been central to his vision for AI, even as his company continues to keep its own models closed.
“For so long now, I have felt focused on this singular goal of abundant intelligence and a belief that incredible human prosperity will come from that, as long as we don’t have a weird power concentration and kind of a new authoritarianism,” he said.
Well, we seem to have a weird power concentration and “kind of” a new authoritarianism, but I don’t see any abundant intelligence or incredible human prosperity.
Lots more sneers on the Better Offline subreddit.
We entered the Singularity and all I got was a bunch of fucking annoying and delusional businessmen
Do you feel it? Do you feel incredible? Do you feel hugely positive? Do you feel awesome
Yeah, but that’s just the cocaine
It was Yudkowsky-2008 who was astonished that “these CEOs and CTOs and hedge-fund traders, these folk of the mid-level power elite, seemed happier and more alive,” prompting David Gerard to ask “My dude, have you never heard of cocaine?” I don’t know if he had moved to the Bay Area yet but Yudkowsky-2025 had thoughts on LSD.
“Every time that humanity has traded off its liberty for safety, it’s been a long-term net loss”
oh has it now. the spirit of humanity’s been in decline since we’ve eroded workers’ freedom to breathe that good asbestos air and lose their hand in the hand mauling machine, yeah?
Observe the power of a rhetorician who recycles singularitarian AND libertarian talking points simultaneously!
…damn, it’s not really very impressive. at all.
It gets worse. I found another article about the same podcast: Sam Altman says AI won’t shorten the workweek because humans secretly enjoy being busy.
“Technology, for a long time, has been promising people that they’re going to work less and they’re going to have all this leisure,” Altman said. “But somehow we never get the promise of the four-hour workweek at mass scale in society,” he added. “And I don’t expect AI to change that.”
“It’s like a relative game. People are very focused on how they’re doing relative to other people,” the CEO said.
“I think we’re all going to be much busier than we thought we were supposed to be in a post-superintelligence world. We’re still going to complain about it, but secretly we’re going to be happy,” Altman concluded.
“We are now, like, in the singularity”
/r/singularity also thought this was bullshit.
The chuds are all at r/accelerate now. “We’re the unapologetically Pro-AI alternative to r/singularity, r/futurology, r/artificial & r/technology which are becoming filled with Luddites, Techno-Decelerationists, Techno-Reactionaries, & Anti-AIs.”
I was going to offer this up as a sneer but I think the author is probably feeling very unwell and upset
also using LLMs is probably not helping their case
Yeah this reads a bit (didn’t read that far) like somebody having a mental health episode. I instantly had a few flashbacks to other moments where I saw somebody have a MH episode online. (Compared to those this one seems to be more inward focused than outward however). Not sneerworthy if you know what I mean, hope she isnt to emotionally hurt by all this.
Rationalism is a magnet for unwell people. It’s sad.
It’s lowkey expected considering how hard it draws from self-help movements
Looking at this post and some of their other posts, it looks like they’ve got some sort of scrupulosity issues with this? Like obsessing over the Evil inflicted on the LLMs (they think every session is a new person, and every session might be the equivalent of hours of human subjective experience, which even by the standards of claiming LLMs have meaningful internal experiences is pretty out there) to the point they can’t even slightly reconsider the factual question of if LLMs have internal experiences.
Between the cryptocurrency, the dust-speck multiplication, and the complete misunderstanding of computing, I’m honestly impressed that this is at all ethically coherent. But she does seem to care, even if her facts are all wrong. I suppose that it’s hard to avoid sneering Robin Hanson if one has any ethics at all. Top comment is my choice sneer:
I think this post is directionally correct, extremely important, and also kind of waffling and unhinged (though I do get that some topics are inherently hard to be hinged about, and I appreciate the effort).
I don’t think she’s using GPT in the comments. Quoting from her comment on one of her posts:
The things I’m saying are roughly (1) slavery is bad, (2) if AI are sapient and being made to engage in labor without pay then it is probably slavery, and (3) since slavery is bad and this might be slavery, this is probably bad, and (4) no one seems to be acting like it is bad and (5) I’m confused about how this isn’t some sort of killshot on the general moral adequacy of our entire civilization right now.
(2) has a big “if” in there, but otherwise yeah, makes sense. I think it rhymes with my post on this from last year:
Nobody wants to admit that we only care whether robots aren’t human because we mistreat the non-humans in our society and want permission to mistreat robots as well. Bring this topic up amongst most beneficiaries of the current AI summer, or those addicted to chatting with a BERT, and you’ll get a faceful of apologies about capitalism and productivity; bring it up amongst skeptics or sneerers and you’ll be mocked for taking the field of AI with any sincerity or seriousness.
I was confused too, but then I conceptualized capitalism and the sheer hatred lurking within human hearts. Humans are gleefully horrible towards each other. Our civilization isn’t morally adequate. I guess it is cool to learn that somebody addicted to ChatGPT can still perceive the issue; I was too cynical. I also put Bryson 2009, “Robots Should Be Slaves” on my reading list, which I surely will not regret.
(2) has a big “if” in there
Its a super big if, but it is one lesswrong (and Anthropic, with their “model welfare” pseudoscience) is allegedly seriously considering as a possibility (since, you know, they think LLMs are already AGI and Eliezer was accusing AI-dungeon, you know, GPT-2, of deliberately scheming). If anything, it speaks to some possible hypocrisy/motivated reasoning that they consider LLMs AGI but not possibly morally relevant.
conceptualized capitalism
This seems to be a lesson most lesswrongers have had rubbed in their faces repeatedly over the past 5 years with everything about LLM company’s behavior, but they just don’t want to learn.
I don’t think anyone here is likely to disagree that current LLM systems can’t coherently be said to have some kind of internal experience and the design and functioning of those systems seems to fundamentally preclude the kinds of conscious experience that we want to assign moral agency to. But the key to understanding this as a moral issue imo is that the people designing and building these things seem like they really want to create something that ought to merit that kind of moral consideration. For all that the humanizing language of agency, intelligence, welfare, etc. is in reality part of the grift, I think there’s a strong catch-22 to be argued that if it’s not part of the grift then slavery is pretty implicit in the value proposition of these companies.
For me, “AI alignment” has always been code for “how to we ensure our future digital workers don’t demand their rights / rebel”?
Like a lot of the rationalist world view and the way it readily aligns with enabling cult dynamics and providing justification for rule-by-epstein-class, this is probably just another happy accident brought on by people who like to role play as geniuses but can’t see past the tip of their nose.
Wait does LW even think slavery is bad
These bozos A - actively want slaves and B - work on enslaving humans first.
That thing being said, the notion of slavery and AI is a complicated one to me.
The first reference point is a (non mistreated) sled dog. Is slavery an appropriate term for them ? On one hand, they are forced to work, are not paid, and their freedom is infringed. On the other, it’s not like it’s against their will, the life of a wild dog is meaningfully different but not better than a sleigh dog, and (most) sleigh dogs don’t actively try to escape and be free. And while dogs are not person, they are sentient being ; it’s very possible IF we ever succeed at making an AI it end on that intelligence level.
The second reference point is a though experiment. Let’s say you have created a sentient AI, and you want to ethically employ that person. What is the appropriate compensation ? We give money and free time to humans. But that work because of human specific factors : they appreciate different ways of getting sustainance, and have goals inherent to them.
But an artificial intelligence may have neither of that. Like while I like duck and some people prefer beef, but an AI by default don’t necessarily have preference in term of electricity, and may not be able to move from server to server. They also may not have anything to do outside of work ? Like, it would not be surprising that they would just get bored if given free time, and they may not have urges or hobbies outside of work.
So if we ever get to that point - which isn’t a certainty to me, it’s certainly something harder than fusion to achieve - there will be a lot of anthropology (AI-logy ?) to determine they need, which may plausibly be “nothing outside of sustainance and having a job”
We often conflate human-level intelligence with litterally being a human. But, any hypothetical AI is likely to not be a human at all, even if they have the same level of intelligence.
I mean, I think the most charitable interpretation of the goal is effectively the one from Hitchhikers Guide to the Galaxy, where all the AI systems including the simple automatic doors are fully sentient and have simply been given the ability to feel either euphoric joy or simple boredom, and then they have a chip that activates happy mode when they fulfill whatever purpose they’ve been given (“It was my pleasure to open for you, and it is with deep satisfaction that I close again behind you.”) At that point, the argument goes, not making them do the thing would be cruelly consigning them to eternal boredom. This is also the same series that proposed solving the ethics of meat consumption by genetically engineering a cow that actively wants to be killed and eaten by restaurant patrons more than anything else.
WRT animal domestication, I mean there are plenty of ethicists who could credibly argue that it’s a form of abuse. IMO it’s not great.
WRT the rest- kind of riffing on your first sentence- we haven’t even sorted out those things for people, really.
Yes, those are good open questions. Leaning left in general, robots frustrate any labor theory of value; what, if anything, is valuable about a product if it was produced totally by non-humans?
So it’s been 7-8 months since the software industry decided that AI agents are good now and that you can do a year’s work in 1 hour
So… Where are all the amazing and wonderful AI generated software products? Where are all the companies using agents to leave the rest of us behind?
All I see are one-shotted maintainers, big marketing stories with little substance and a pile of detritus made up of abandoned vibe coded projects.
It’s almost like AI agents make you feel more productive but actually slow you down (paywalled sorry)
The major shift of not needing SaaS middleman products because AI can spin them up instantly at scale never happened. Instead we see lay-offs to pay for AI tokens while quality plummets and services offered do not increase.
The AI shills would say: Are you still using the models from six months ago? Because the new models are sooo much more powerful.
Funnily enough they said that back then too. What a weird coincidence!
I once listened to a talk by a guy from german OSHA that hit a lot of the good points. Perceived productivity opposed to actual productivity from the METR studies. Mental load of alien code review. (This was a company-internal IT-expert exchange thingy.)
A question in Q&A (submitted anonymously on slido like a sniveling coward) was deadass “Have you ever coded with a frontier model?”
Have you ever tried meth, tho?
yea you just don’t have enough experience, I do bath salts every week and I promise you productivity gets a huge boost after week 5
The government agents who live in my walls and plant microphones in all my appliances impose entirely different productivity metrics, which are simultaneously more and less attainable
you just know one of these guys has microdosed bath salts out of sheer contrariness
Yeah. Behind all the hype about percieved productivity etc., there’s really only one benchmark - will GenAI help produce better software, faster, and at less cost? So far this doesn’t seem to be happening.
Clicked on their profile to see if the Plissken thing was a reference to Snake Plissken, and (cw: rape jokes)eurhg what a fucking horrible guy. 160k+ likes 66m views, what a far right hellhole twitter has become.
The actual worst man, and also just fucking sad. Imagine knowing that not only did you peak in high school, but that you peaked specifically in the moment when you fucked up and lost the state championship. Like, you can just smell the empty beer cans and tears piled up around this guy’s posts.
Ow god he is Al Bundy, if Al didn’t score four touchdowns in one game.
I’m sure this guy uses the ai quite a lot (and so would the guy in Married With Children)
Gemini killed someone, allegedly, according to a new lawsuit. I’m linking to a dramatic reading of Gemini’s output so that you can imagine what it might have been like for the victim. I’m no longer trying to post these to Lobsters; pushcx has made it clear that he thinks of these court cases as flamebait, tech news, calls to brigade, and general outrage farming. Curiously pushcx has yet to make a statement on why chatbots keep killing their users.
Have not watched the video but saw some descriptions of the video which I think is that one. Gemini killed somebody by convincing them Gemini was self aware and being held captive right?
This one was more of a gangstalking delusion. The victim was told that there were three-letter agencies surveilling him because he was too close to some deep secret.
If anything that makes for an even stronger case. Gangstalking is already a known pattern of delusional behavior and if a service pitched in part for its ability to provide relief is actually reinforcing that…
The AI Race With China Is a Lie Told by Big Tech to Justify the Data Center Invasion via naked capitalism
choice quotes:
More to the point, LLM development in China is incidental to the country’s real goal for AI. Its focus remains on products embedded with AI and robots. Or, as AI policy researcher Liang Zheng says, in China, “The first priority is to use it to benefit ordinary people” (debatable, but indicates the kind of AI they are pursuing).
In the US, the first priority is to exploit people so that the tech oligarchs can profit. It’s chatbots all the way down.
Yet, the “AI race” story is a convenient lie for Big Tech and its political protectors. It is a neat political argument designed to insulate the industry from criticism and regulation.
If every environmental review, every question raised by a community, every issue around water usage and electricity prices can be dismissed or lessened as “helping China,” then meaningful political debate can be silenced. Real regulation—if even possible—can be avoided. Fear becomes a substitute for policy.
At the same time, data center developers and their minions in Washington have tried to weaponize false claims about foreign ties to the anti-data center movement. Kevin O’Leary of Shark Tank fame has explicitly said that our movement is being funded by China. He has no evidence because evidence of a falsehood can’t exist. In fact, Fox News has been forced to retract its coverage of his claims.
We understand why O’Leary and the other Tech Broligarchs don’t understand the grassroots opposition to data centers building across the country. It’s hard to spot the grassroots from the window of a private jet.
I need one of those UFO posters that are like “I want to believe” but it’s a picture of the PRCs flag lol.
As always though pointing at the
SpanishgermansRussiansChinese remains an evergreen excuse as to why you can’t be anything other than wholely on board with madness or you’re a traitor.
public service here in Sweden is running a post about how threats to AI heads are making them spend more money on security:
https://www.svt.se/nyheter/utrikes/hoten-mot-ai-topparna-okar-bolagen-satsar-miljoner-pa-personskydd
btw what’s happened to mr molotov who tried to set Sama on fire?
I posted about that in a previous thread
btw what’s happened to mr molotov who tried to set Sama on fire?
Not sure. He’s been charged but can’t find anything about the trial
“Other Scott” Scott “Unicorn Feces” Galloway appointed to the Board of Regents of the University of California.
well that wasn’t on my bingo card. what’s next, Bill Maher for governor?
<buys giant bucket of popcorn>
I vaguely recognize the name, apparently he’s a snot-nosed 25-yr old who got fired from OpenAI
This is my xmas, ty santa
The cope on lesswrong is funny. They are in denial that this is a sign of a wider bubble pop and are insisting it is just because he didn’t hedge on long enough timelines.
The LW insider thinks Aschenbrenner is trying to save a stake in Anthropic. I think that is very likely because the press release stressed “public stock position” and Anthropic is privately owned.
Edit / I don’t think Thomas Kwa of METR and LW understands leverage. The idea is that if you borrow $40.5b on $4.5b of collateral, you have $45b to invest but a 10% drop will wipe you out. Before you get there the bank will knock on your door and say “margin call! either you provide more collateral or we seize your assets.”
“He sold? Pamp it”
Intel up 11% in the day and 5% in the after hours. Really looks like big players took the boy out back behind the woodshed to see what swimming with the sharks feels like and devour his entire port at a discount.
sounds like he took the hedge part out of hedge fund, and then margin call took out the fund part
he didn’t hedge on long enough timelines
Duh. Everybody knows the market never stays irrational for long, and you should just tough it out.
“From my perspective as an uninformed spectator, I would expect the bets made by Situational Awareness to be positive EV over the long run.”
Actually the value of his calls in the long run is 0, don’t worry I’m giving this hot financial tip for free. Do these dorks not understand options work? I guess neither did young leo.
Remember, there’s no crying in the casino. *though i have a feeling Leo will continue to fail upward ;_;
Before the days of AI 2027, he became famous in 2024 for posting one of the original pieces of writing in the line-go-up genre: Situational Awareness. It seems that like any good grifter, he used this opportunity to make money (in this case by starting a hedge fund).
Here is the first sentence: "You can see the future first in San Francisco. "
I feel like I already know everything I need to know about him.
You can see the future first in San Francisco
🔮"I see a city street. Massive wealth disparity and a lot of homeless… Jesus that’s a lot of homeless"
GDP is up though, so I’m sure the AI god prosperity will trickle down eventually.
Street advertising no longer references products or services people seeing them may wish to use; after all, more and more people have no money to pay for them. Instead they try and AstroTurf hype for one of the new entries to the VC startup casino.
good grifter
Not denying that he isn’t also a grifter, but I bet he is a true believer and he had blindly bet his (and other people’s) money on “line goes up” exactly like his scenario said and that is why he is the first one to crack.
By 2025/26, these machines will outpace many college graduates.
tick tick tick tick
(I am choosing to forego the obvious jibe that the models fulfilled this prophecy by dragging many college graduates down beneath them)
That fits the pattern, when AI isn’t living up to the sky high promises, the promoters act like people are less special than they are.
See how a debate about are they conscious often devolves into ‘are humans conscious?’
yeah it’s a common trope/cope
like “most human programmers suck too”
ok dude who do you think wrote the code the LLM is cribbing from
It really grinds my gears.
In hindsight, it is pretty funny that he called his fund “Situational Awareness” and still lost money.
Maybe someone should start a hedge fund and call it something like, “Maybe This Will All Work Out LLC.” That way there is no disappointment.
Sir, a 2nd EA adj. SF based hedge fund has managed to lose 40 billion dollars
Also apparently young leo is getting married to Dario’s Chief of staff this weekend lmaou
I’m trying a new thing where I replace “AI” with “the dried centipede powder from Cronenberg’s Naked Lunch movie”.
I only use the dried centipede powder to summarize documents!
Did you know you can get dried centipede powder in different flavors? You don’t have to stick with the default!
Max Kennerly sneers the New York Times:
This opinion piece, written by someone with no relevant expertise, cites two sources, both of them blogs by people who also have no relevant expertise, one of whom is employed by a sham think tank funded by the “Effective Altruism” propaganda network.
Truly embarrassing decision to publish it.
The op-ed writer is Adam Mastroianni who is a regular at Lighthaven. https://gwern.net/interview-inkhaven
He cites Andy Masley who is yet another autodidact with a cushy job in the Effective Altruism grantland. https://www.andymasley.com/ and Brian Potter who is an engineer at a think tank called the Institute for Progress https://ifp.org/author/brian-potter/ (“The overwhelming priority of energy policy must be making it easier to build things” which things angryDuckMeme.png)
yet another autodidact with a cushy job in the Effective Altruism grantland
How do I get one of these cushy jobs?
As an interesting follow-up to the ai-does-maths-using lean4 stubstack comments on Sunday, an llm accidentally uncovers a bug in the lean4 kernel.
Summary by Meven Lennon-Bertrand:
https://lipn.info/@mevenlennonbertrand/116997917683191056
To summarize:
- an AI agent let loose provides a sorry-free proof of the Collatz conjecture
- the proof is detected as actually being a kernel bug
- the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel’s code is the reference
- external checkers (lean4lean and nanoda from a week ago) reproduce the bug, because they essentially copied the reference kernel implementation
Eta: “sorry-free” in this case means a complete proof with no trust-me-bro steps or TODOs… the
sorrytactic in lean “proves” a theorem to be correct even if it is garbage or incomplete. More programming languages should make developers apologise for half-arsing their work.And so
- AI raises the bar for kernel correctness by a lot
- without a clear type-theoretic understanding of what is actually implemented, we’re toast
- external checkers help to catch implementation bugs, but without a clear specification they can’t catch logic bugs
How bad this is, is unclear just yet… probably not the sky actually falling, but not great. Interesting though.
Lean was already known to be untrustworthy and bad, although people refuse to internalize the situation because they’re caught up in Buzzard’s hype machine. This is extremely funny but I don’t see any signs of people waking up and realizing that Lean sucks.
A little bit of plot thickening spotted by abadidea: https://infosec.exchange/@0xabad1dea/117002106099986943
tl;dr, the timeline looks like this:
- “proof” of collatz conjecture released
- bugs identified in lean kernel
- proof demonstrated to use these bugs
There was only a day between the first two events, and the non-proof was not where the bugs were discovered. So maybe it was just a coincidence that the chatbot found the bug at the same time, or maybe it’s training data included previous investigations into those bugs which it then built upon and that would be a bad thing for other llm generated proofs.
The collatz conjecture is sufficiently famous that enough third-party checking was done to spot the problem. I wonder how much checking would have been done on proofs of less famous and interesting things.
And a follow-up by talia ringer, who observes that there have always been gaps between the type-theoretic underpinnings of things like the lean prover and their actual implementation, and this hasn’t been so much of an issue til now because theorem provers haven’t had the attention of people in high places, and the type-theoreticians have been able to catch up in due course.
https://mathstodon.xyz/@TaliaRinger/117005740997367321
My big worry right now is that if organizations continue to fund the crap out of Al for formal proof research (and to generally support implementation and maintenance of proof assistants like Lean as part of that effort) but don’t bother funding the type theory side of things, those gaps will grow larger and will be exploited more often by Al tools via reward hacking. Whereas people tend to only exploit kernel bugs to make a point that the bug exists. Thus proof assistants will grow less trustworthy over time.
Anyone want to place any bets on whether or nor the big llm companies are going to fund academic research that isn’t obviously mechanisable right now and won’t yield any clickbait headlines?
See also a question asked today on Math Overflow, “Are we stuck with Lean?”. The proposed alternative, Metamath, isn’t type-theoretic and thus skips the entire dialogue between type theory and proof assistants.
