@screwlisp @tao @Ardubal

No.

The automatic theorem proving blokes were writing programs that actually tried to do mathematics. LLMs are exactly and only random text generators. Since they have a lot of math proofs in their training data, they randomly mimic math proofs quite nicely.

LLMs do not have a mechanism for checking their output. That's your job.

Lean, on the other hand, is about computer representation of proofs; building libraries of valid proof steps. Serious work. Not a joke.

# Akkoma # Statistics 2026-05-07 01:00 CEST
Number of active instances: 675
Number of users: 20 326
Number of statuses: 9 107 085
Number of users last 4h: 4
Number of statuses last 4h: 1509

# Fediverse

Microsoft Edge Stores Passwords In Plaintext In RAM https://yro.slashdot.org/story/26/05/06/2014204/microsoft-edge-stores-passwords-in-plaintext-in-ram?utm_source=rss1.0mainlinkanon

"Murmuration over Lanhydrock Park", 2020 by Annie Ovenden, English painter

#WomensArt

Throw in the New York Times for good measure:

https://www.theguardian.com/media/2026/may/05/new-york-times-lawsuit-equal-opportunity

I understand that these stories sound ridiculous to you, but you need to grasp what it MEANS that it is not some random loon making these arguments - it's the US government. In effect, the US government is now working to enforce white male heteronormative supremacy, by making the argument that any policy designed to fight that supremacy, is actually discrimination and legally actionable racism against well, them.

How about learning some Norwegian and moving away from Big Tech at the same time?

More and more are wanting to get away from Big Tech. Are you ready?

#Norway #Digital #Dugnad #Vivaldi #Browser

https://digitaldugnad.eu

It’s happening!

As of right now, I am testing Thunderbird Pro services.

I have been waiting for this moment since forever. I am euphoric! Let’s hope it lives up to my expectations 👀

#Thundermail #Thunderbird #ThunderbirdPro #EarlyBird #TBpro #Stalwart #Appointment #Send

Stephen Colbert interviewed Barack Obama last night and I watched some of it with 15 to show her what it was like when she and her brother were born. And then I apologized for what things have become.

15: he’s so NORMAL

#USPol

@yaelwrites I know you have one on mine :-)

@ausfestivus still not sure if you’re talking about the queer music playing gadget (complimentary) or the train

May I introduce to you:
His cuteness, Monsieur Pepe.
#catsofmastodon

Little Snitch is finally on Linux. Learn how to use this eBPF firewall to monitor outbound traffic, block telemetry, and see how it compares to OpenSnitch.

Full guide here: https://ostechnix.com/little-snitch-for-linux/

#Littlesnitch #Firewall #Security #Linux

Sony to Pay Almost $4 Billion for Bieber, Neil Young Catalog
https://www.bloomberg.com/news/articles/2026-05-06/sony-to-pay-almost-4-billion-for-bieber-neil-young-catalog?utm_source=flipboard&utm_medium=activitypub

Posted into Bloomberg Asia @bloomberg-asia-bloomberg

@iftas @anewsocial doesn't seem to belong on this list

@natematias There is a lot of mileage around base rates. I wrote a toy model on a similar AI detection problem in ecology. You use AI to detect pest species and trap them. We'd expect AI to have some chance of errors, the consequences of which depend on base rates. Under the model trapping changes the base rates leading to unintended consequences.

https://www.sciencedirect.com/science/article/pii/S030438002600102X

In a three day period the US DoJ has gone after two major liberal universities, places with infinite dollars, based on expressly nazi arguments about gender and "reverse racism."

I don't think people are understanding yet. This is what I meant when I said "he might be MORE dangerous now that he knows he's finished."

he is gonna try to speed run turning our society into the 3rd Reich. How fast? Not sure, but he might seriously mean "before November."

It has taken far too long to get to this point. But it's also pretty cool having three fully functional Xserves running! (None booted when I got them)

RE: https://hachyderm.io/@thomasfuchs/116530074619109826

If the events in ‘Tuvix’ had involved Elon Musk and Jeff Bezos, Hugo Drax would have stepped out of the transporter

Hormuz Crisis Shows Gaps in Taiwan’s High-Tech ‘Silicon Shield’
https://www.bloomberg.com/news/features/2026-05-06/hormuz-crisis-shows-gaps-in-taiwan-s-high-tech-silicon-shield?utm_source=flipboard&utm_medium=activitypub

Posted into Economics @economics-bloomberg