this post was submitted on 26 Jul 2026
18 points (100.0% liked)
TechTakes
2623 readers
88 users here now
Big brain tech dude got yet another clueless take over at HackerNews etc? Here's the place to vent. Orange site, VC foolishness, all welcome.
This is not debate club. Unless it’s amusing debate.
For actually-good tech, you want our NotAwfulTech community
founded 3 years ago
MODERATORS
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 sorry tactic 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.
LLM bros actively force themselves everywhere, part infinity:
Newgrounds moderation had to deal with someone (probably a scammer) posting slop "art advice" recently - exactly why, nobody fuckin' knows:
Transcript/desciption
I've already passed it off to folks that could nuke the account from orbit, but I guess as a public service announcement, be on the lookout for replies in the forums that sound a little too LLM-y.
An account (unsure if a bot or just a weirdo) recently attempted to infiltrate the art forum, giving plausible-sounding AI-generated list-based advice, complete with preambles and summations, exactly the kind of syntax and format one would expect if they've dealt with enough clanker slop text. It fooled a small handful of people, but it was extremely easy to confirm my suspicions as soon as I smelled the clanker stank on it. One click made it clear that they had a generated PFP and profile linking to some image slopification scam.
It raises the question, what would anyone possibly have to gain from posting slop on the forums? It seems like a really stupid thing to do, but I guess braindead behavior tracks, given who we're dealing with. Make sure "helpful" new users aren't just trying to Dead Internet us or whatever.
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)
zerohedge sponcon so obviously a grift but wtf is this AI Black Paper by Jim Rickards
https://www.zerohedge.com/sponsored-post/sobering-july-29th-announcement-set-crush-ai-stocks
Have the goldbugs been reading Zitron? or just an extremely late pivot from btc to ai? or flooding the zone?
Anyway who the hell is Jim Rickards? Another week, another guy.
https://en.wikipedia.org/wiki/Talk:James_Rickards
"AI Black Paper" is catchy enough though, should be a goth band.
or flooding the zone?
With Zerohedge I think this is most likely. Maintaining truthiness by predicting 30 out of the last 2 recessions.
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/
[Removed by Moderator]
Ah, that's probably better for my mental health I guess
never thought id see r/moralityscaling and r/whowouldcirclejerk here ever lol. but christ alive why would you ever conceive of this
Jesus fucking christ none of these people should be having sex
There is some pedophilia in there too.
…also, what the fuck. This is a step backwards, even just reading it. I’m mad.
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.
load more comments
(5 replies)
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 ~~Spanish~~ ~~germans~~ ~~Russians~~ Chinese remains an evergreen excuse as to why you can't be anything other than wholely on board with madness or you're a traitor.
view more: next ›